Changeset 2186 for src

Timestamp:

Jul 16, 2012, 4:59:09 PM (9 years ago)

Author:

tranquil

Message:

updated joint semantics

Location:

src

Files:

• RTL/RTL_paolo.ma (modified) (1 diff)
• common/StructuredTraces.ma (modified) (7 diffs)
• joint/Joint_paolo.ma (modified) (1 diff)
• joint/Traces.ma (moved) (moved from src/joint/as_semantics.ma) (2 diffs)
• joint/blocks.ma (modified) (1 diff)
• joint/semantics_blocks.ma (modified) (2 diffs)
• joint/semantics_paolo.ma (modified) (22 diffs)

src/RTL/RTL_paolo.ma

@@ -59 +59 @@
 definition rtl_statement ≝ joint_statement rtl_params.
 
-interpretation "move" 'mov r a = (MOVE ? ? (mk_Prod ? rtl_argument r a)).
+interpretation "move" 'mov r a = (MOVE rtl_params ? (mk_Prod ? rtl_argument r a)).
 
 (* aid unification *)

src/common/StructuredTraces.ma

@@ -334 +334 @@
 qed.
 
-(* an uncalling, unreturning and *unjumping*,
-  as well as unlabelled (but possibly for the first and last statuses) 
-  possibly empty trace segment *)
-inductive trace_any_any (S:abstract_status) : S → S → Type[0] ≝
-  | taa_base :
+(*
+(* an trace of unlabeled and cl_other states, possibly empty *)
+inductive trace_no_label_any (S:abstract_status) : S → S → Type[0] ≝
+  | tna_base :
       ∀start_status: S.
-        trace_any_any S start_status start_status
-  | taa_step :
+      ¬as_costed … start_status →
+      trace_no_label_any S start_status start_status
+  | tna_step :
       ∀status_pre: S.
       ∀status_init: S.
       ∀status_end: S.
         as_execute S status_pre status_init →
-        trace_any_any S status_init status_end →
         as_classifier S status_pre cl_other →
-        ¬as_costed … status_init →
-          trace_any_any S status_pre status_end.
-
-let rec taa_status_list S st1 st2 (taa : trace_any_any S st1 st2) on taa : list S ≝
+        ¬as_costed … status_pre →
+        trace_no_label_any S status_init status_end →
+          trace_no_label_any S status_pre status_end.
+
+let rec tna_append_tna S st1 st2 st3 (taa1 : trace_no_label_any S st1 st2)
+  on taa1 :
+    trace_no_label_any S st2 st3 →
+    trace_no_label_any S st1 st3 ≝
+  match taa1 with
+  [ tna_base st1' H ⇒ λtaa2.taa2
+  | tna_step st1' st2' st3' H G K tl ⇒
+    λtaa2.tna_step ???? H G K (tna_append_tna … tl taa2)
+  ].
+
+definition tna_non_empty ≝ λS,st1,st2.λtna : trace_no_label_any S st1 st2.
+  match tna with
+  [ tna_base _ _ ⇒ false
+  | tna_step _ _ _ _ _ _ _ ⇒ true
+  ].
+
+coercion tna_to_bool : ∀S,st1,st2.∀tna:trace_no_label_any S st1 st2.bool ≝
+ tna_non_empty on _tna : trace_no_label_any ??? to bool.
+
+lemma tna_unlabelled : ∀S,st1,st2.trace_no_label_any S st1 st2 → ¬as_costed … st1.
+#S #st1 #st2 * [#st #H @H | #st #st' #st'' #_ #_ #H #_ @H] qed.
+
+let rec tna_append_tal S st1 fl st2 st3 (tna : trace_no_label_any S st1 st2)
+  on tna :
+  trace_any_label S fl st2 st3 →
+  if tna then Not (as_costed … st2) else True →
+  trace_any_label S fl st1 st3 ≝
+  match tna return λst1,st2.λx : trace_no_label_any S st1 st2.
+    ∀fl,st3.
+    trace_any_label S fl st2 st3 →
+    if x then Not (as_costed … st2) else True →
+    trace_any_label S fl st1 st3
+  with
+  [ tna_base st1' H ⇒ λfl,st3,taa2,prf.taa2
+  | tna_step st1' st2' st3' H G K tl ⇒ λfl,st3,taa2,prf.
+    tal_step_default ????? H (tna_append_tal ????? tl taa2 ?) G (tna_unlabelled … tl)
+  ] fl st3.
+  cases (tna_non_empty … tl) [@prf|%]
+  qed.
+*)
+
+inductive trace_any_any (S : abstract_status) : S → S → Type[0] ≝
+  | taa_base : ∀st.trace_any_any S st st
+  | taa_step : ∀st1,st2,st3.
+    as_execute S st1 st2 →
+    as_classifier S st1 cl_other →
+    ¬as_costed S st2 →
+    trace_any_any S st2 st3 →
+    trace_any_any S st1 st3.
+
+definition taa_non_empty ≝ λS,st1,st2.λtaa : trace_any_any S st1 st2.
   match taa with
-  [ taa_base st1' ⇒ [st1']
-  | taa_step st1' st2' st3' _ tl _ _ ⇒ st1' :: taa_status_list … tl
+  [ taa_base _ ⇒ false
+  | taa_step _ _ _ _ _ _ _ ⇒ true
   ].
 
-let rec taa_append_taa S st1 st2 st3 (taa1 : trace_any_any S st1 st2)
-  on taa1 : trace_any_any S st2 st3 → trace_any_any S st1 st3 ≝
-  match taa1
-  return λst1,st2.λx : trace_any_any S st1 st2.
-    trace_any_any S st2 st3 → trace_any_any S st1 st3
-  with
-  [ taa_base _ ⇒ λtaa2.taa2
-  | taa_step st1' st2' st3' H tl G K ⇒ λtaa2.
-      taa_step … H (taa_append_taa … tl taa2) G K
-  ].
-
-let rec taa_append_tal S st1 fl st2 st3 (taa : trace_any_any S st1 st2)
-  on taa :
+coercion taa_to_bool : ∀S,st1,st2.∀taa:trace_any_any S st1 st2.bool ≝
+ taa_non_empty on _taa : trace_any_any ??? to bool.
+
+let rec taa_append_tal S st1 fl st2 st3
+  (taa : trace_any_any S st1 st2) on taa :
   trace_any_label S fl st2 st3 →
   trace_any_label S fl st1 st3 ≝
-  match taa
-  return λst1,st2.λx : trace_any_any S st1 st2.
-    trace_any_label S fl st2 st3 → trace_any_label S fl st1 st3
+  match taa return λst1,st2.λx : trace_any_any S st1 st2.
+    ∀fl,st3.
+    trace_any_label S fl st2 st3 →
+    trace_any_label S fl st1 st3
   with
-  [ taa_base _ ⇒ λtaa2.taa2
-  | taa_step st1' st2' st3' H tl G K ⇒ λtaa2.
-      tal_step_default … H (taa_append_tal … tl taa2) G K
-  ].
+  [ taa_base st1' ⇒ λfl,st3,tal2.tal2
+  | taa_step st1' st2' st3' H G K tl ⇒ λfl,st3,tal2.
+    tal_step_default ????? H (taa_append_tal ????? tl tal2) G K
+  ] fl st3.
+
+interpretation "trace any any label append" 'append taa tal = (taa_append_tal ????? taa tal).
 
 let rec tlr_rel S1 st1 st1' S2 st2 st2'
@@ -416 +461 @@
     fl2 = doesnt_end_with_ret ∧
     ∃st2mid,taa,H,G,K.
-    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
+    tal2 ≃ taa_append_tal ? st2 ??? taa
       (tal_base_not_return ? st2mid st2' H G K)
   | tal_base_return st1 st1' _ _ ⇒
@@ -437 +482 @@
     tal_rel … tl1 tal2 (* <- this makes it many to many *)
   ].
-  
+
 interpretation "trace any label rel" 'napart t1 t2 = (tal_rel ???????? t1 t2).
 interpretation "trace label label rel" 'napart t1 t2 = (tll_rel ???????? t1 t2).
-interpretation "trace label return rel" 'napart t1 t2 = (tlr_rel ???????? t1 t2).
-
+interpretation "trace label return rel" 'napart t1 t2 = (tlr_rel ?????? t1 t2).
+
+let rec taa_rel_inv S1 fl1 st1 st1mid st1' S2 fl2 st2 st2'
+  (taa1 : trace_any_any S1 st1 st1mid) on taa1 :
+  ∀tal1 : trace_any_label S1 fl1 st1mid st1'.
+  ∀tal2 : trace_any_label S2 fl2 st2 st2'.
+  tal_rel … (taa1 @ tal1) tal2 →
+  tal_rel … tal1 tal2 ≝ ?.
+cases taa1 -taa1
+[ -taa_rel_inv //
+| #st #st' #st'' #H #G #K #tl #tal1 #tal2 whd in ⊢ (%→?);
+  @(taa_rel_inv … tl)
+]
+qed.
+
+let rec tlr_rel_transitive S1 st1 st1' S2 st2 st2' S3 st3 st3'
+  (tlr1 : trace_label_return S1 st1 st1')
+  (tlr2 : trace_label_return S2 st2 st2')
+  (tlr3 : trace_label_return S3 st3 st3') on tlr1 :
+  tlr_rel … tlr1 tlr2 → tlr_rel … tlr2 tlr3 → tlr_rel … tlr1 tlr3 ≝
+match tlr1 with
+  [ tlr_base st1' st1'' tll1 ⇒ ?
+  | tlr_step st1' st1'' st1''' tll1 tl1 ⇒ ?
+  ]
+and tll_rel_transitive S1 fl1 st1 st1' S2 fl2 st2 st2' S3 fl3 st3 st3'
+  (tll1 : trace_label_label S1 fl1 st1 st1')
+  (tll2 : trace_label_label S2 fl2 st2 st2')
+  (tll3 : trace_label_label S3 fl3 st3 st3') on tll1 :
+  tll1 ≈ tll2 → tll2 ≈ tll3 → tll1 ≈ tll3 ≝
+  match tll1 with
+  [ tll_base fl1' st1' st1'' tal1 H ⇒ ?
+  ]
+and tal_rel_transitive S1 fl1 st1 st1' S2 fl2 st2 st2' S3 fl3 st3 st3'
+  (tal1 : trace_any_label S1 fl1 st1 st1')
+  (tal2 : trace_any_label S2 fl2 st2 st2')
+  (tal3 : trace_any_label S3 fl3 st3 st3') on tal1 :
+  tal1 ≈ tal2 → tal2 ≈ tal3 → tal1 ≈ tal3 ≝
+  match tal1 with
+  [ tal_base_not_return st1' st1'' H G K ⇒ ?
+  | tal_base_return st1' st1'' H G ⇒ ?
+  | tal_base_call st1' st1'' st1''' H G K tlr1 L ⇒ ?
+  | tal_step_call fl1' st1' st1'' st1''' st1'''' H G L tlr1 K tl1 ⇒ ?
+  | tal_step_default fl1' st1' st1'' st1''' H tl1 G K ⇒ ?
+  ].
+[1,2: cases tlr2 #st2' #st2'' [1,3: #tllhd2 |2,4: #st2''' #tllhd2 #tlrtl2]
+  [2,3: *] normalize in ⊢ (%→?); [ #Rhd12 | * #Rhd12 #Rtl12 ]
+  cases tlr3 #st3' #st3'' [1,3: #tllhd3 |2,4: #st3''' #tllhd3 #tlrtl3]
+  [2,3: *] normalize in ⊢ (%→?); [ #Rhd23 | * #Rhd23 #Rtl23 ] whd
+  [ @(tll_rel_transitive … Rhd12 Rhd23) |
+    %{(tll_rel_transitive … Rhd12 Rhd23)}
+    @(tlr_rel_transitive … Rtl12 Rtl23) 
+  ]
+|3:
+  cases tll2 #fl2' #st2' #st2'' #tal2 #H2 * #G2 #R12
+  cases tll3 #fl3' #st3' #st3'' #tal3 #H3 * #G3 #R23
+  %{(tal_rel_transitive … R12 R23)} //
+|*:
+  [1,2,3: * #EQ]
+  [5: whd in ⊢ (%→?→%); @tal_rel_transitive]
+  *#st2mid *#taa2
+  [ *#H2 *#G2 *#K2 #R12
+  | *#H2 *#G2 #R12
+  | *#st2' *#H2 *#G2 *#K2 *#tlr2 *#L2 *#R12 #R12'
+  | *#st2' *#st2'' *#H2 *#G2 *#K2 *#tlr2 *#L2 *#tl2 ** #R12 #R12' #R12''
+  ] destruct #R23 lapply (taa_rel_inv … R23) [1,2: // |3: *#EQ destruct]
+  *#st3mid *#taa3
+  [ *#st3' *#H3 *#G3 *#K3 *#tlr3 *#L3 *#R23 #R23'
+    %{(refl …)} %{st3mid} %{taa3} %{st3'} %{H3} %{G3} %{K3} %{tlr3} %{L3}
+    %{R23} @(tlr_rel_transitive … R12' R23')
+  | *#st3' *#st3'' *#H3 *#G3 *#K3 *#tlr3 *#L3 *#tl3 ** #R23 #R23' #R23''
+    %{st3mid} %{taa3} %{st3'} %{st3''} %{H3} %{G3} %{K3} %{tlr3} %{L3} %{tl3}
+    %{(tal_rel_transitive … R12'' R23'')}
+    %{R23} @(tlr_rel_transitive … R12' R23')
+  ]
+]
+qed.
 
 let rec flatten_trace_label_label
@@ -507 +626 @@
   S st1 fl st2 st3 (taa : trace_any_any S st1 st2) on taa :
   ∀tal : trace_any_label S fl st2 st3.
-    flatten_trace_any_label … (taa_append_tal … taa tal) =
+    flatten_trace_any_label … (taa @ tal) =
       flatten_trace_any_label … tal ≝ ?.
 cases taa -st1 -st2
-[ #st1 #tal %
-| #st_pre #st_init #st2 #H #taa #G #K #tal
-  whd in match (taa_append_tal ???????);
+[ //
+| #st_pre #st_init #st2 #H #G #K #taa' #tal
+  whd in match (? @ ?);
   whd in ⊢ (??%?); //
 ]
-qed.  
-
+qed.
 
 let rec tll_rel_to_traces_same_flatten
@@ -606 +724 @@
   λS : abstract_status. (Σl.∃pc.as_label_of_pc S pc = Some ? l) → ℕ.
 
-definition lift_cost_map_id :
-  ∀S_in, S_out: abstract_status.
-   (∀l. (∃pc.as_label_of_pc S_out pc = Some … l) +
-       ¬(∃pc.as_label_of_pc S_out pc = Some … l)) →
-  (as_cost_map S_out) → as_cost_map S_in ≝ λS_in,S_out,dec,m,l_sig.
-   match dec l_sig with
-   [ inl prf ⇒ m «l_sig, prf»
-   | inr _ ⇒ 0 (* labels not present in out code get 0 *)
+definition lift_sigma_map_id :
+  ∀A,B : Type[0].∀P_in,P_out : A → Prop.B →
+    (∀a.P_out a + ¬ P_out a) →
+  ((Σa.P_out a) → B) → (Σa.P_in a) → B ≝ λA,B,P_in,P_out,dflt,dec,m,a_sig.
+   match dec a_sig with
+   [ inl prf ⇒ m «a_sig, prf»
+   | inr _ ⇒ dflt (* labels not present in out code get 0 *)
    ].
 
-lemma lift_cost_map_id_eq :
-  ∀S_in, S_out, dec, m, l_in, l_out.
-  pi1 ?? l_in = pi1 ?? l_out → lift_cost_map_id S_in S_out dec m l_in = m l_out.
-#S_in #S_out #dec #m #l_in * #l_out #prf #EQ
-whd in match lift_cost_map_id; normalize nodelta
-cases (dec l_in) normalize nodelta >EQ
-[2: #H @⊥] /2 by refl, absurd/
+lemma lift_sigma_map_id_eq :
+  ∀A,B,P_in,P_out,dflt,dec,m,a_in,a_out.
+  pi1 ?? a_in = pi1 ?? a_out →
+  lift_sigma_map_id A B P_in P_out dflt dec m a_in = m a_out.
+#A#B#P_in#P_out#dflt#dec#m#a_in#a_out#EQ
+whd in match lift_sigma_map_id; normalize nodelta
+cases (dec a_in) normalize nodelta >EQ cases a_out
+#a #H #G [ % | @⊥ /2 by absurd/ ]
 qed.
 
@@ -631 +749 @@
   with precedence 20
 for @{'fold plus 0 (λ${ident i}:$X.true) (λ${ident i}:$Y. $f) $l}.
+
+definition lift_cost_map_id :
+  ∀S_in,S_out : abstract_status.? →
+  as_cost_map S_out → as_cost_map S_in
+  ≝
+ λS_in,S_out : abstract_status.
+  lift_sigma_map_id costlabel ℕ
+    (λl.∃pc.as_label_of_pc S_in pc = Some ? l)
+    (λl.∃pc.as_label_of_pc S_out pc = Some ? l)
+    0.
 
 lemma lift_cost_map_same_cost :
@@ -645 +773 @@
   #EQ destruct
   whd in ⊢(??%%);
-  >(lift_cost_map_id_eq … e0)
+  whd in match lift_cost_map_id; normalize nodelta
+  >(lift_sigma_map_id_eq ????????? e0)
   >e0 in e1; normalize in ⊢(%→?); #EQ
   >(IH … EQ) %

src/joint/Joint_paolo.ma

@@ -181 +181 @@
   match s with
   [ GOTO l ⇒ Labels … [l]
-  | _ ⇒ Labels … [ ] (* tailcalls will need to be integrated in structured traces *)
+  | tailcall _ ⇒ Call (* tailcalls will need to be integrated in structured traces *)
+  | _ ⇒ Labels … [ ]
   ].
 

src/joint/Traces.ma

@@ -1 +1 @@
 include "joint/semantics_paolo.ma".
-include "common/StructuredTraces.ma".
 
-definition stmt_classifier :
-  ∀p : params.∀globals.
-    (ext_step p → status_class) →
-    (ext_fin_stmt p → status_class) →
-    joint_statement p globals → status_class
-  ≝ λp,globals,ext_step_classifier,ext_fin_step_classifier,s.
-  match s with
-  [ sequential stp _ ⇒
-    match stp with
-    [ COND _ _ ⇒ cl_jump
-    | extension ext_s ⇒ ext_step_classifier ext_s
-    | CALL_ID _ _ _ ⇒ cl_call (* Paolo : this does not take into account external calls! *)
-    | _ ⇒ cl_other
-    ]
-  | final stp ⇒
-    match stp with
-    [ RETURN ⇒ cl_return
-    | extension_fin ext_s ⇒ ext_fin_step_classifier ext_s
-    | _ ⇒ cl_other
-    ]
-  ].
+record evaluation_params : Type[1] ≝
+ { globals: list ident
+ ; sparams:> sem_params
+ ; exit: cpointer
+ ; ev_genv: genv globals sparams
+ ; io_env : state sparams → ∀o:io_out.res (io_in o)
+ } .
+
+(*record classifier_params : Type[1] ≝
+  { cl_pars :> evaluation_parameters
+  ; cl_ext_step : ext_step cl_pars → status_class
+  ; cl_ext_fin_stmt : ext_fin_stmt cl_pars → status_class
+  }.*)
+
 
 definition cpointerDeq ≝ mk_DeqSet cpointer eq_pointer ?.
@@ -30 +22 @@
 ]
 qed.
-  
+
+let rec io_evaluate O I X (env : ∀o.res (I o)) (c : IO O I X) on c : res X ≝
+  match c with
+  [ Value x ⇒ OK … x
+  | Interact o f ⇒
+    ! i ← env o ;
+    io_evaluate O I X env (f i)
+  | Wrong e ⇒ Error … e
+  ].
+
+definition cost_label_of_stmt :
+  ∀p : evaluation_params.joint_statement p (globals p) → option costlabel ≝
+  λp,s.match s with
+  [ sequential s _ ⇒
+    match s with
+    [ step_seq s ⇒
+      match s with
+      [ COST_LABEL lbl ⇒ Some ? lbl
+      | _ ⇒ None ?
+      ]
+    | _ ⇒ None ?
+    ]
+  | _ ⇒ None ?
+  ].
+
 definition joint_abstract_status :
- ∀p : evaluation_parameters.
- (ext_step p → status_class) →
- (ext_fin_stmt p → status_class) →
- abstract_status ≝ 
- λp,ext_step_cl,ext_fin_step_cl.
+ ∀p : evaluation_params.
+ abstract_status ≝
+ λp.
  mk_abstract_status
    (* as_status ≝ *) (state_pc p)
-   (* as_execute ≝ *) (λs1,s2.eval_state … p (genv2 p) s1 = return s2)
+   (* as_execute ≝ *)
+    (λs1,s2.io_evaluate … (io_env p s1) (eval_state … p (ev_genv p) s1) = return s2)
    (* as_pc ≝ *) cpointerDeq
    (* as_pc_of ≝ *) (pc …)
    (* as_classifier ≝ *)
-    (λs,cl.∃stmt.fetch_statement ? p … (genv2 p) (pc … s) = return stmt ∧
-     stmt_classifier … ext_step_cl ext_fin_step_cl stmt = cl)
+    (λs,cl.∃stmt.fetch_statement ? p … (ev_genv p) (pc … s) = return stmt ∧
+     stmt_classifier … stmt = cl)
    (* as_label_of_pc ≝ *)
     (λpc.
-      match fetch_statement ? p … (genv2 p) pc with
-      [ OK stmt ⇒
-        match stmt with
-        [ sequential s _ ⇒
-          match s with
-          [ COST_LABEL l ⇒ Some ? l
-          | _ ⇒ None ?
-          ]
-        | _ ⇒ None ?
-        ]
+      match fetch_statement ? p … (ev_genv p) pc with
+      [ OK stmt ⇒ cost_label_of_stmt … stmt
       | _ ⇒ None ?
       ])
    (* as_after_return ≝ *)
-    (λs1,s2. (* Paolo: considering sequential calls, tailcalls are out of the picture for now *)
-      ∃stp,nxt.fetch_statement ? p … (genv2 p) (pc … s1) = return (sequential ?? stp nxt) ∧
+    (λs1,s2.
+      (* Paolo: considering sequential calls, tailcalls must be classified as cl_return *)
+      ∃stp,nxt.fetch_statement ? p … (ev_genv p) (pc … s1) = return (sequential ?? stp nxt) ∧
       succ_pc p p (pc … s1) nxt = return pc … s2)
-   (* as_final ≝ *) (λs.is_final (globals ?) p (genv2 p) (exit p) s ≠ None ?).
+   (* as_final ≝ *) (λs.is_final (globals ?) p (ev_genv p) (exit p) s ≠ None ?).

src/joint/blocks.ma

@@ -176 +176 @@
   ∀p:stmt_params.∀g.∀l:bind_new (localsT p) (list (joint_seq p g)).bind_seq_block p g (joint_step p g) ≝
   bind_seq_list_bind_seq_block on _l : bind_new ? (list (joint_seq ??)) to bind_seq_block ?? (joint_step ??).
+
+notation > "x ~❨ B , l ❩~> y 'in' c" with precedence 56 for
+  @{'block_in_code $c $x $B $l $y}.
+  
+notation < "hvbox(x ~❨ B , l ❩~> y \nbsp 'in' \nbsp break c)" with precedence 56 for
+  @{'block_in_code $c $x $B $l $y}.
+
+definition step_in_code ≝
+  λp,globals.λc : codeT p globals.λsrc : code_point p.λs : joint_step p globals.
+  λdst : code_point p.
+  ∃nxt.stmt_at … c src = Some ? (sequential … s nxt) ∧
+       point_of_succ … src nxt = dst.
+
+definition fin_step_in_code ≝
+  λp,globals.λc : codeT p globals.λsrc : code_point p.λs : joint_fin_step p.
+  stmt_at … c src = Some ? (final … s).
+
+let rec seq_list_in_code p globals (c : codeT p globals)
+  (src : code_point p) (B : list (joint_seq p globals))
+  (l : list (code_point p)) (dst : code_point p) on B : Prop ≝
+  match B with
+  [ nil ⇒
+    match l with
+    [ nil ⇒ src = dst
+    | _ ⇒ False
+    ]
+  | cons hd tl ⇒
+    match l with
+    [ nil ⇒ False
+    | cons mid rest ⇒
+      step_in_code …  c src hd mid ∧ seq_list_in_code … c mid tl rest dst
+    ]
+  ].
+
+interpretation "seq list in code" 'block_in_code c x B l y = (seq_list_in_code ?? c x B l y).
+
+lemma seq_list_in_code_append :
+  ∀p,globals.∀c : codeT p globals.∀src,B1,l1,mid,B2,l2,dst.
+  src ~❨B1,l1❩~> mid in c → mid ~❨B2,l2❩~> dst in c →
+  src ~❨B1@B2,l1@l2❩~> dst in c.
+#p #globals #c #src #B1 lapply src -src elim B1
+[ #src * [2: #mid' #rest] #mid #B2 #l2 #dst [*] #EQ normalize in EQ; destruct(EQ)
+  #H @H
+| #hd #tl #IH #src * [2: #mid' #rest] #mid #B2 #l2 #dst * #H1 #H2
+  #H3 %{H1 (IH … H2 H3)}
+]
+qed.
+
+lemma seq_list_in_code_append_inv :
+  ∀p,globals.∀c : codeT p globals.∀src,B1,B2,l,dst.
+  src ~❨B1@B2,l❩~> dst in c →
+  ∃l1,mid,l2.l = l1 @ l2 ∧ src ~❨B1,l1❩~> mid in c ∧ mid ~❨B2,l2❩~> dst in c.
+#p #globals #c #src #B1 lapply src -src elim B1
+[ #src #B2 #l #dst #H %{[ ]} %{src} %{l} %{H} % %
+| #hd #tl #IH #src #B2 * [2: #mid #rest] #dst * #H1 #H2
+  elim (IH … H2) #l1 * #mid' * #l2 ** #G1 #G2 #G3
+  %{(mid::l1)} %{mid'} %{l2} %{G3} >G1 %{(refl …)}
+  %{H1 G2}
+]
+qed.
+
+definition seq_block_step_in_code ≝
+  λp,g.λc:codeT p g.λsrc.λB : seq_block p g (joint_step p g).λl,dst.
+  src ~❨\fst B, \fst l❩~> \snd l in c ∧ step_in_code … c (\snd l) (\snd B) dst.
+
+definition seq_block_fin_step_in_code ≝
+  λp,g.λc:codeT p g.λsrc.λB : seq_block p g (joint_fin_step p).λl.λdst : unit.
+  src ~❨\fst B, \fst l❩~> \snd l in c ∧ fin_step_in_code … c (\snd l) (\snd B).
+
+(* generates ambiguity even if it shouldn't
+interpretation "seq block step in code" 'block_in_code c x B l y = (seq_block_step_in_code ?? c x B l y).
+interpretation "seq block fin step in code" 'block_in_code c x B l y = (seq_block_fin_step_in_code ?? c x B l y).
+*)
 
 (*

src/joint/semantics_blocks.ma

@@ -1 +1 @@
 include "joint/blocks.ma".
-include "joint/semantics_paolo.ma".
-
-
-axiom ExecutingInternalCallInBlock : String.
-
-let rec seq_list_labels p g (b : list (joint_step p g)) on b : list label ≝
+include "joint/Traces.ma".
+
+(* let rec seq_list_labels p g (b : list (joint_step p g)) on b : list label ≝
   match b with
   [ nil ⇒ [ ]
   | cons hd tl ⇒ step_labels … hd @ seq_list_labels … tl
-  ].
-
-definition step_flow_change_labels :
-  ∀p,g,lbls1,lbls2.(∀x.In ? lbls1 x → In ? lbls2 x) →
-    step_flow p g lbls1 → step_flow p g lbls2 ≝
-  λp,g,lbls1,lbls2,prf,flow.
-  match flow with
-  [ Redirect l ⇒ Redirect ??? «l, prf ? (pi2 … l)»
-  | Init id b args dest ⇒ Init … id b args dest
-  | Proceed ⇒ Proceed ???
-  ].
-
-coercion step_flow_diff_lbls :
-  ∀p,g,lbls1,lbls2.(∀x.In ? lbls1 x → In ? lbls2 x) →
-  ∀flow : step_flow p g lbls1.step_flow p g lbls2 ≝
-  step_flow_change_labels on _flow : step_flow ??? to step_flow ???.
-
-definition monad_step_flow_times_coerc :
-  ∀p,g,lbls1,lbls2,M,A.(∀x.In ? lbls1 x → In ? lbls2 x) →
-    monad M ((step_flow p g lbls1) × A) → monad M ((step_flow p g lbls2) × A) ≝
-    λp,g,lbls1,lbls2,M,A,H,m.
-    ! 〈flow,a〉 ← m ;
-    return 〈(flow : step_flow ?? lbls2),a〉. assumption qed.
-
-coercion step_flow_monad_times :
-  ∀p,g,lbls1,lbls2,M,A.(∀x.In ? lbls1 x → In ? lbls2 x) →
-    ∀m : monad M ((step_flow p g lbls1) × A).monad M ((step_flow p g lbls2) × A) ≝
-  monad_step_flow_times_coerc on _m : monad ? ((step_flow ???) × ?) to monad ? ((step_flow ???) × ?).
-
-let rec eval_seq_list globals (p:sem_params) (ge : genv globals p)
-  (st : state p) (b : list (joint_step p globals)) on b :
-    IO io_out io_in ((step_flow p globals (seq_list_labels … b)) × (state p)) ≝
-    match b return λx.IO ?? ((step_flow ?? (seq_list_labels … x)) × ?) with
-    [ nil ⇒ return 〈Proceed ???, st〉
-    | cons hd tl ⇒
-      ! 〈flow, st'〉 ← eval_step … ge st hd ;
-      match flow return λ_.IO ?? ((step_flow ?? (seq_list_labels … (hd :: tl))) × ?) with
-      [ Proceed ⇒ eval_seq_list globals p ge st' tl
-      | _ ⇒ return 〈flow, st'〉
-      ]
-    ]. /2 by Exists_append_r, Exists_append_l/ qed.
-
-definition fin_step_flow_change_labels :
-  ∀p,g,lbls1,lbls2.(∀x.In ? lbls1 x → In ? lbls2 x) →
-    fin_step_flow p g lbls1 → fin_step_flow p g lbls2 ≝
-  λp,g,lbls1,lbls2,prf,flow.
-  match flow with
-  [ FRedirect l ⇒ FRedirect ??? «l, prf ? (pi2 … l)»
-  | FTailInit id b args ⇒ FTailInit … id b args
-  | FEnd ⇒ FEnd ???
-  ].
-
-coercion fin_step_flow_diff_lbls :
-  ∀p,g,lbls1,lbls2.(∀x.In ? lbls1 x → In ? lbls2 x) →
-  ∀flow : fin_step_flow p g lbls1.fin_step_flow p g lbls2 ≝
-  fin_step_flow_change_labels on _flow : fin_step_flow ??? to fin_step_flow ???.
-
-definition monad_fin_step_flow_times_coerc :
-  ∀p,g,lbls1,lbls2,M,A.(∀x.In ? lbls1 x → In ? lbls2 x) →
-    monad M ((fin_step_flow p g lbls1) × A) → monad M ((fin_step_flow p g lbls2) × A) ≝
-    λp,g,lbls1,lbls2,M,A,H,m.
-    ! 〈flow,a〉 ← m ;
-    return 〈(flow : fin_step_flow ?? lbls2),a〉. assumption qed.
-
-coercion fin_step_flow_monad_times :
-  ∀p,g,lbls1,lbls2,M,A.(∀x.In ? lbls1 x → In ? lbls2 x) →
-    ∀m : monad M ((fin_step_flow p g lbls1) × A).monad M ((fin_step_flow p g lbls2) × A) ≝
-  monad_fin_step_flow_times_coerc on _m : monad ? ((fin_step_flow ???) × ?) to monad ? ((fin_step_flow ???) × ?).
-
-definition block_cont_labels ≝ λp,g,ty.λb : block_cont p g ty.
-  seq_list_labels … (\fst b) @
-  match ty return λx.stmt_type_if ? x ??? → ? with
-  [ SEQ ⇒ step_labels …
-  | FIN ⇒ fin_step_labels …
-  ] (\snd b).
-
-definition eval_block_cont :
-  ∀globals.∀p : sem_params.∀ty.genv globals p →
-  state p → ∀b : block_cont p globals ty.
-  IO io_out io_in (
-    (stmt_type_if ? ty step_flow fin_step_flow p globals (block_cont_labels … b)) ×
-    (state p)) ≝ λglobals,p,ty,ge,st.
-  match ty return λx.∀b : block_cont p globals x.
-    IO io_out io_in (
-      (stmt_type_if ? x step_flow fin_step_flow p globals (block_cont_labels … b)) ×
-      (state p))
-  with
-  [ SEQ ⇒ λb.
-    ! 〈flow, st'〉 ← eval_seq_list globals p ge st (\fst b) ;
-    match flow return λ_.IO ?? (step_flow … ((block_cont_labels … b))×?) with
-    [ Redirect l ⇒ return 〈Redirect ??? «l,?», st'〉
-    | Proceed ⇒ eval_step … ge st' (\snd b)
-    | Init _ _ _ _ ⇒
-      Error … (msg ExecutingInternalCallInBlock)
-    ]
-  | FIN ⇒ λb.
-    ! 〈flow, st'〉 ← eval_seq_list globals p ge st (\fst b) ;
-    match flow return λ_.IO ?? ((fin_step_flow … (block_cont_labels … b))×?) with
-    [ Redirect l ⇒ return 〈FRedirect ??? «l,?», st'〉
-    | Proceed ⇒ eval_fin_step … ge st' (\snd b)
-    | Init _ _ _ _ ⇒
-      Error … (msg ExecutingInternalCallInBlock)
-    ]
-  ]. try cases l /2 by Exists_append_r, Exists_append_l/ qed.
-
-(*
-lemma m_pred
-
-lemma attach_m_pred_bind : ∀M.∀MP : MonadPred P.∀P,X,Y.m : monad M X.
-  ∀f : X → monad M Y.m_pred MP P … m →
-  ! x ← m ; f x = ! x ←  
-*)
-
-definition no_init : ∀p,globals,lbls,A.((step_flow p globals lbls)×A)→Prop ≝
-  λp,globals,lbls,A,flp.
-  match \fst flp with
-  [ Init _ _ _ _ ⇒ False
-  | _ ⇒ True
-  ].
-
-definition truly_sequential : ∀p,globals,lbls,A.((step_flow p globals lbls)×A)→Prop ≝
-  λp,globals,lbls,A,flp.
-  match \fst flp with
-  [ Proceed ⇒ True
-  | _ ⇒ False
-  ].
-
-definition never_calls : ∀p : sem_params.∀globals.genv globals p → joint_step p globals → Prop ≝
-λp,globals,ge,s.match s with
-[ CALL_ID f args dest ⇒
-  Try
-    ! b ← find_symbol … ge f ;
-    ! fd ← find_funct_ptr … ge b ;
-    match fd with
-    [ Internal _ ⇒ return False
-    | External _ ⇒ return True
-    ]
-  catch ⇒
-    True
-| extension c ⇒
-  ∀st : state p.
-  pred_io … (λ_.True) (no_init …) (exec_extended … ge c st)
-| _ ⇒ True
-].
-
-definition unbranching ≝ λp,globals,ge,s.never_calls p globals ge s ∧ step_labels … s = [ ].
-
-lemma err_to_io_bind : ∀O,I,X,Y.∀m : res X.∀f : X → res Y.
-  err_to_io O I ? (! x ← m ; f x) = ! x ← m : IO O I X ; f x.
-#O #I #X #Y * //
-qed.
-
-lemma pred_io_True : ∀O,I,X,m.pred_io O I X (λ_.True) (λ_.True) m.
-#O #I #X #m elim m // qed.
-
-(*
-lemma pred_res_True : ∀X,m.pred_res X (λ_.True) (λ_.True) m.
-#X #m elim m // qed.
-*)
-
-(*
-lemma never_calls_no_init : ∀p,globals,ge,s.
-  never_calls p globals ge s →
-  ∀st : state p.
-  pred_io … (λ_.True) (no_init …) (eval_step … ge st s).
-#p#g#ge * //
-[10,12:
-|*:
-  #a #b #c try #d try #e try #f try #g
-  @res_io_pred
-  @(mp_bind … (λ_.True) … (pred_res_True …))
-  #st *  try (@mp_return @I)
-  @(mp_bind … (λ_.True) … (pred_res_True …))
-  #st * [9: elim st] normalize nodelta try (@mp_return @I)
-  @(mp_bind … (λ_.True) … (pred_res_True …))
-  #st *  try (@mp_return @I)
-  @(mp_bind … (λ_.True) … (pred_res_True …))
-  #st * [elim (opaccs ????) #by1 #by2 normalize nodelta]
-  @(mp_bind … (λ_.True) … (pred_res_True …))
-  #st * [2: elim (op2 ?????) #by #bit  normalize nodelta]
-  try (@mp_return @I)
-  @(mp_bind … (λ_.True) … (pred_res_True …))
-  #st * @mp_return @I
-]
-[ #id #args #dest #H whd in H;
-  #st change with (! x ← ? ; ?) in match (eval_step ?????);
-  elim (find_symbol ???) in H ⊢ %; [//]
-  #b >m_return_bind  >m_return_bind
-  change with (! x ← ? ; ?) in match (eval_call_block ?????????);
-  elim (find_funct_ptr ???) [//]
-  #fd >m_return_bind  >m_return_bind
-  elim fd #fn normalize nodelta *
-  @(mp_bind … (λ_.True)) [//]
-  #st * @(mp_bind … (λ_.True) … (pred_io_True …))
-  #st * @(mp_bind … (λ_.True) … (pred_io_True …))
-  #st * @(mp_bind … (λ_.True) … (pred_io_True …))
-  #st * @mp_return %
-| #s #H @H
-]
-qed.
-
-lemma unbranching_truly_sequential : ∀p,globals,ge,s.
-  unbranching p globals ge s →
-  ∀st : state p.
-  pred_io … (λ_.True) (truly_sequential …) (eval_step … ge st s).
-#p#globals#ge#s * #H #G #st
-lapply (never_calls_no_init … H st) @m_pred_mp
->G * *
-[ * #lbl * | #id #fd #args #dest ] #st * %
-qed.
-*)
-
-lemma seq_list_labels_append : ∀p,globals,b1,b2.
-  seq_list_labels p globals (b1 @ b2) =
-  seq_list_labels … b1 @ seq_list_labels … b2.
-#p #g #b1 elim b1
-[ //
-| #hd #tl #IH #b2 whd in ⊢ (??%%);
-  >associative_append <IH %
-]
-qed.
-
-(*
-lemma eval_seq_list_append : ∀globals,p,ge,st,b1,b2.
-  eval_seq_list globals p ge st (b1@b2) =
-  ! 〈flow, st'〉 ← eval_seq_list … ge st b1 ;
-  match flow with
-  [ Proceed ⇒
-    ! 〈flow',st''〉 ← eval_seq_list … ge st' b2 ;
-    return 〈(flow' : step_flow … (seq_list_labels … (b1@b2))), st''〉
-  | _ ⇒ return 〈(flow : step_flow … (seq_list_labels … (b1@b2))), st'〉
-  ].
-[2,3,4:
-  #lbl #H >seq_list_labels_append
-  [1,2: @Exists_append_l | @Exists_append_r ] @H ]
-#globals#p#ge#st#b1 lapply st -st elim b1
-[ #st #b2 >m_return_bind normalize nodelta
-  <(m_bind_return … (eval_seq_list … b2)) in ⊢ (??%?);
-  @m_bind_ext_eq ** 
-  [ * #lbl #H | #id #fd #args #dest ] #st' %
-| #hd #tl #IH #st #b2
-  whd in match (? @ b2);
-  whd in match (eval_seq_list ?????);
-  whd in match (eval_seq_list ???? (hd :: tl));
-  >m_bind_bind
-  @m_bind_ext_eq
-  ** [ #lbl | #id #fd #args #dest] #st' normalize nodelta
-  [1,2: @m_return_bind]
-  >m_bind_bind
-  >IH >m_bind_bind
-  @m_bind_ext_eq **
-  [#lbl | #id #fd #args #dest ] #st' normalize nodelta
-  >m_return_bind
-  [1,2: @m_return_bind ]
-  >m_bind_bind normalize nodelta
-  @m_bind_ext_eq **
-  [#lbl|#id #fd #args #dest] #st'' >m_return_bind %
-]
-qed.
-
-lemma eval_seq_list_unbranching :
-∀globals,p,ge,st,b.
-  All ? (unbranching … ge) b →
-  pred_io … (λ_.True) (truly_sequential …)
-    (eval_seq_list globals p ge st b).
-#globals#p#ge#st #b lapply st -st elim b
-[ #st * %
-| #hd #tl #IH #st * #hd_ok #tl_ok
-  @mp_bind
-  [2: @(unbranching_truly_sequential … hd_ok st) |]
-  ** [#lbl|#id#fd#args#dest] #st' *
-  normalize nodelta
-  @mp_bind [2: @(IH st' tl_ok)|]
-  ** [#lbl|#id#fd#args#dest] #st'' * %
-]
-qed.
-
-lemma io_pred_as_rel : ∀O,I,A,Perr,P,v.
-  pred_io O I A Perr P v →
-  rel_io O I (eq …) … (λx,y.x = y ∧ P x) v v.
-#O #I #A #Perr #P #v elim v
-[ #o #f #IH whd in ⊢ (%→%);
-  #H %{(refl …)} #i @IH @H
-|*: /2/
-]
-qed.
-
-lemma eval_seq_list_append_unbranching : ∀globals,p,ge,st,b1,b2.
-  All ? (unbranching … ge) b1 →
-  eval_seq_list globals p ge st (b1@b2) =
-  ! 〈flow, st'〉 ← eval_seq_list … ge st b1 ;
-  ! 〈flow', st''〉 ← eval_seq_list … ge st' b2 ;
-  return 〈(flow' : step_flow … (seq_list_labels … (b1@b2))), st''〉.
-[2: #lbl #H >seq_list_labels_append @Exists_append_r @H ]
-#globals #p #ge #st #b1 #b2 #H
->eval_seq_list_append
-@mr_bind
-[2: @(io_pred_as_rel … (eval_seq_list_unbranching … H)) |]
-** [#lbl|#id#fd#args#dest] #st
-#y * #EQ <EQ -y * @rel_io_eq normalize nodelta %
-qed.
-*)
-lemma block_cont_labels_append : ∀p,globals,ty,b1,b2.
-  block_cont_labels p globals ty (b1 @ b2) =
-  block_cont_labels … b1 @ block_cont_labels … b2.
-#p #g #ty * #l1 #s1 * #l2 #s2
-whd in match (〈?,?〉@?); whd in ⊢ (??%?);
->seq_list_labels_append
->associative_append
->associative_append
->associative_append %
-qed.
-(*
-lemma eval_block_cont_append : ∀globals.∀p : sem_params.∀ty,ge,st.
-  ∀b1 : block_cont p globals SEQ.∀b2 : block_cont p globals ty.
-  eval_block_cont ??? ge st (b1@b2) =
-  ! 〈flow, st'〉 ← eval_block_cont ??? ge st b1 ;
-  match ty return λx.
-    block_cont p globals x → IO ?? ((stmt_type_if ? x  step_flow fin_step_flow ???) × ?) with
-  [ SEQ ⇒ λb2.
-    match flow with
-    [ Proceed ⇒ 
-      ! 〈flow',st''〉 ← eval_block_cont … ge st' b2 ;
-      return 〈?, st''〉
-    | Redirect l ⇒ return 〈Redirect ??? «l,?», st'〉
-    | _ ⇒ Error … (msg ExecutingInternalCallInBlock)
-    ]
-  | FIN ⇒ λb2.
-    match flow with
-    [ Proceed ⇒ 
-      ! 〈flow',st''〉 ← eval_block_cont … ge st' b2 ;
-      return 〈?, st''〉
-    | Redirect l ⇒ return 〈FRedirect ??? «l,?», st'〉
-    | _ ⇒ Error … (msg ExecutingInternalCallInBlock)
-    ]
-  ] b2.
-[3,5: whd in flow'; @flow'
-  #lbl >block_cont_labels_append @Exists_append_r
-|2,4: cases l -l #l >block_cont_labels_append @Exists_append_l
-]
-#globals#p * whd in match stmt_type_if; normalize nodelta
-#ge#st * #l1 #s1 * #l2 #s2
-whd in match (〈?,?〉@?);
-whd in match eval_block_cont; normalize nodelta
->m_bind_bind
->eval_seq_list_append
->m_bind_bind
-@m_bind_ext_eq
-
- whd in ⊢ (??%?);
-    match ty return λx.IO ?? ((stmt_type_if ? x ?????) × ?) with
-    [ SEQ ⇒ 
-    | FIN ⇒ return 〈FRedirect ??? «l,?», st'〉
-    ]
-  | _ ⇒ Error … (msg ExecutingInternalCallInBlock)
-  ].
-#globals#p#ty#ge#st*#l1#s1*#l2#s2
-whd in match (〈?,?〉@?);
-whd in match eval_block_cont; normalize nodelta
->m_bind_bind
->eval_seq_list_append
->m_bind_bind
-@m_bind_ext_eq
-** [#l|#id#fd#args#dest] normalize nodelta #st'
-[1,2:>m_return_bind normalize nodelta
-  [ >m_return_bind ] % ]
-change with (! x ← ? ; ?) in match (eval_seq_list ???? (?::?));
->m_bind_bind whd in match stmt_type_if;
-normalize nodelta
->m_bind_bind
-@m_bind_ext_eq
-**[#l|#id#fd#args#dest] normalize nodelta #st''
-[1,2: >m_return_bind normalize nodelta % | % ]
-qed.
-*)
-
-
-(* just like repeat, but without the full_exec infrastructure, and it
-   stops upon a non-proceed flow cmd *)
-let rec repeat_eval_state_flag n globals (p:sem_params) (ge : genv globals p)
-  (st : state_pc p) on n :
-    IO io_out io_in (bool × (state_pc p)) ≝
-match n with
-[ O ⇒ return 〈false,st〉
-| S k ⇒
-  ! 〈flag,st'〉 ← eval_state_flag globals p ge st ;
-  if flag then return 〈true,st'〉 else repeat_eval_state_flag k globals p ge st'
-].
-
-definition block_size : ∀p,g,ty.block_cont p g ty → ℕ ≝
-λp,g,ty,b.S (|\fst b|).
-
-interpretation "block cont size" 'norm b = (block_size ??? b).
-
-lemma repeat_eval_state_flag_plus : ∀n1,n2,globals, p, ge, st.
-  repeat_eval_state_flag (n1 + n2) globals p ge st =
-  ! 〈flag,st〉 ← repeat_eval_state_flag n1 globals p ge st ;
-  if flag then return 〈true, st〉 else repeat_eval_state_flag n2 globals p ge st.
-#n1 elim n1 -n1 [| #n1 #IH]
-#n2 #globals #p #ge #st
-[ @m_return_bind
-| change with (! st' ← ? ; ?) in match (repeat_eval_state_flag (S ?) ????);
-  change with (! st' ← ? ; ?) in match (repeat_eval_state_flag (S n1) ????);
-  >m_bind_bind in ⊢ (???%);
-  @m_bind_ext_eq ** #st' normalize nodelta
-  [ % | @IH ]
-]
-qed.
-
-lemma repeat_eval_state_flag_one : ∀globals, p, ge, st.
-  repeat_eval_state_flag 1 globals p ge st = eval_state_flag globals p ge st.
-#globals #p #ge #st
-change with (! st' ← ? ; ?) in match (repeat_eval_state_flag (S ?) ????);
-<(m_bind_return … (eval_state_flag ????)) in ⊢ (???%);
-@m_bind_ext_eq ** #st %
-qed.
-
-lemma eval_tunnel_step :
-  ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,dst.
-  fetch_function … ge (pc … st) = OK … fn →
-  point_of_pointer ? p … (pc … st) = OK … src →
-  src ~~> dst in joint_if_code … fn →
-  eval_state_flag g p ge st =
-    return 〈true,set_pc … (pointer_of_point ? p (pc … st) dst) st〉.
-#p #g #ge #st #fn #src #dst #fetch_fn #pc_pt * #lbl * #EQ1 #EQ2
-change with (! s ← ? ; ?) in match (eval_state_flag ????);
-change with (! fn ← ? ; ?) in match (fetch_statement ?????);
->pc_pt in ⊢ (??%?); >m_return_bind
->fetch_fn in ⊢ (??%?); >m_return_bind
->EQ1 in ⊢ (??%?);  >m_return_bind
->EQ2 in ⊢ (??%?);
-change with (! st ← ? ; ?) in match (eval_statement ?????);
-whd in match eval_fin_step; normalize nodelta
->m_return_bind
-whd in match eval_fin_step_flow; normalize nodelta
-change with (! ptr ← ? ; ?) in match (goto ??????);
-whd in match pointer_of_label_in_block; normalize nodelta
-whd in match fetch_function in fetch_fn;
-normalize nodelta in fetch_fn; 
->fetch_fn in ⊢ (??%?); >m_return_bind
->EQ2 in ⊢ (??%?); >m_return_bind
-cases st #st' ** #ty ** #id #H #o #EQ destruct(EQ)
-elim (pointer_compat_from_ind … H) %
-qed.
-
-lemma fetch_function_from_block_eq :
-  ∀p,g,ge.
-  ∀ptr1,ptr2 : cpointer. pblock ptr1 = pblock ptr2 →
-  fetch_function p g ge ptr1 = fetch_function p g ge ptr2.
-#p #g #ge #ptr1 #ptr2 #EQ
-whd in match fetch_function; normalize nodelta >EQ
-@m_bind_ext_eq // qed.
-
-(*
-lemma eval_tunnel :
-  ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,dst.
-  fetch_function … ge (pc … st) = OK … fn →
-  point_of_pointer ? p … (pc … st) = OK … src →
-  src ~~>^* dst in joint_if_code … fn →
-  ∃n.repeat_eval_state n g p ge st =
-    return 〈f,set_pc … (pointer_of_point ? p (pc … st) dst) st〉.
-#p #g #ge #st #fn #src #dst #fetch_fn #pc_pt * #through
-lapply pc_pt -pc_pt lapply fetch_fn -fetch_fn lapply src -src lapply st -st
-elim through [2: #hd #tl #IH]
-#st #src #fetch_fn #pc_pt
-[2: #EQ <EQ %{0}
-  >(pointer_of_point_of_pointer … (refl …) pc_pt) cases st // ]
-* #H1 #H2
-letin st' ≝ (set_pc p (pointer_of_point p p (pc p st) hd) st)
-elim (IH st' … H2)
-[3: >fetch_function_from_block_eq [@fetch_fn ||] whd in match st';
-  @pointer_of_point_block
-|2:
-  whd in match st'; >point_of_pointer_of_point %
-]
-#n' #EQ %{(S n')}
-change with (! st1 ← ? ; ?) in match (repeat_eval_state ?????);
->(eval_tunnel_step … fetch_fn pc_pt H1) >m_return_bind
->EQ %
-qed.
-
-lemma eval_tunnel_plus :
-  ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,dst.
-  fetch_function … ge (pc … st) = OK … fn →
-  point_of_pointer ? p … (pc … st) = OK … src →
-  src ~~>^+ dst in joint_if_code … fn →
-  ∃n.repeat_eval_state (S n) g p ge st =
-    return set_pc … (pointer_of_point ? p (pc … st) dst) st.
-#p #g #ge #st #fn #src #dst #fetch_fn #pc_pt * #mid * #H1 #H2
-letin st' ≝ (set_pc p (pointer_of_point p p (pc p st) mid) st)
-elim (eval_tunnel … ge st' … H2)
-[3: >fetch_function_from_block_eq [@fetch_fn ||] whd in match st';
-  @pointer_of_point_block
-|2:
-  whd in match st'; >point_of_pointer_of_point %
-]
-#n #EQ %{n}
-change with (! st1 ← ? ; ?) in match (repeat_eval_state ?????);
->(eval_tunnel_step … fetch_fn pc_pt H1) >m_return_bind
->EQ %
-qed.
-*)
+  ].*)
 
 lemma fetch_statement_eq : ∀p:sem_params.∀g.∀ge : genv g p.∀ptr : cpointer.
@@ -522 +18 @@
 >EQ1 >m_return_bind >EQ3 %
 qed.
-(*
-lemma eval_seq_list_in_code :
-  ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,B,dst.
-  fetch_function … ge (pc … st) = OK … fn →
-  point_of_pointer ? p … (pc … st) = OK … src →
-  All ? (never_calls … ge) B →
-  seq_list_in_code … (joint_if_code … fn) src B dst →
-  repeat_eval_state_flag (|B|) g p ge st =
-   ! 〈flow,st'〉 ← eval_seq_list g p ge st B ;
-   match flow with
-   [ Redirect l ⇒
-     ! st'' ← goto ?? ge l st' (pblock … (pc ? st)) ;
-     return 〈true, st''〉
-   | Init id fn args dest ⇒ Error … (msg ExecutingInternalCallInBlock)
-       (* dummy, never happens *)
-   | Proceed ⇒
-     let nxt_ptr ≝ pointer_of_point p p … (pc … st) dst in
-     return 〈false, mk_state_pc ? st' nxt_ptr〉
-   ].
-#p #g #ge #st #fn #src #B lapply src -src
-lapply st -st elim B [|#hd #tl #IH]
-#st #src #dst #fetch_fn #pc_pt * [2: #hd_ok #tl_ok]
-[2: #EQ normalize in EQ; <EQ
-  whd in match (eval_seq_list ???? [ ]);
-  >m_return_bind normalize nodelta
-  >(pointer_of_point_of_pointer … (refl …) pc_pt) cases st //
-|1: * #n * #EQat #H
-  change with (! st' ← ? ; ?) in match (eval_seq_list ?????);
-  change with (! st' ← ? ; ?) in match (repeat_eval_state_flag ?????);
-  >m_bind_bind
-  >(fetch_statement_eq … fetch_fn pc_pt EQat) >m_return_bind
-  >m_bind_bind >m_bind_bind
-  lapply (never_calls_no_init … hd_ok st) #hd_ok'
-  @(mr_bind …
-    (λfst1,fst2.fst1 = fst2 ∧ no_init … fst1))
-  [ lapply hd_ok' elim (eval_step ?????)
-    [ #o #f #IH'
-      whd in ⊢ (%→%); #G
-      %{(refl …)} #i @IH' @G
-    |*: #v whd in ⊢ (%→%); #H
-      % [ % ] @H
+
+include alias "basics/logic.ma".
+lemma io_evaluate_bind : ∀O,I,X,Y,env.
+∀m : IO O I X.∀f : X → IO O I Y.
+io_evaluate O I Y env (! x ← m ; f x) =
+! x ← io_evaluate O I X env m ;
+io_evaluate O I Y env (f x).
+#O #I #X #Y #env #m elim m
+[ #o #g #IH #f whd in match (! x ← Interact ????? ; ?);
+  change with (! y ← ? ; ?) in ⊢ (??%(????%?));
+  >m_bind_bind @m_bind_ext_eq #i @IH
+| #x #f %
+| #e #f %
+]
+qed.
+
+lemma fetch_function_from_block_eq :
+  ∀p,g,ge.
+  ∀ptr1,ptr2 : cpointer. pblock ptr1 = pblock ptr2 →
+  fetch_function p g ge ptr1 = fetch_function p g ge ptr2.
+#p #g #ge #ptr1 #ptr2 #EQ
+whd in match fetch_function; normalize nodelta >EQ
+@m_bind_ext_eq // qed.
+
+let rec repeat_eval_seq_no_pc
+  (p : evaluation_params) env
+  (l : list (joint_seq p (globals p))) on l :
+  state p → res (state p) ≝
+  λst.match l with
+  [ nil ⇒ return st
+  | cons hd tl ⇒
+    ! st' ← io_evaluate … (env st) (eval_seq_no_pc (globals p) p (ev_genv p) st hd) ;
+    repeat_eval_seq_no_pc p env tl st'
+  ].
+
+lemma err_to_io_evaluate : ∀O,I,X,env,m.
+  io_evaluate O I X env (err_to_io … m) = m.
+#O#I#X#env * // qed.
+
+definition list_not_empty ≝ λA.λl : list A.match l with [ nil ⇒ false | _ ⇒ true ].
+
+definition no_call_nor_label : ∀p,g.joint_seq p g → bool ≝
+  λp,g,s.match s with
+  [ COST_LABEL _ ⇒ false
+  | CALL_ID _ _ _ ⇒ false
+  | extension_call _ ⇒ false
+  | _ ⇒ true
+  ].
+
+lemma no_call_nor_label_proceed : ∀p : evaluation_params.
+∀st : state p. ∀s.
+no_call_nor_label p (globals p) s →
+eval_seq_pc (globals p) p (ev_genv p) st s = return Proceed ???.
+#p #st * // [ #f #args #dest | #c ] *
+qed.
+
+lemma no_call_nor_label_other : ∀p : evaluation_params.∀s.
+no_call_nor_label p (globals p) s →
+step_classifier … s = cl_other.
+#p * // [ #f #args #dest | #c ] *
+qed.
+
+lemma no_call_nor_label_uncosted : ∀p : evaluation_params.∀s,nxt.
+no_call_nor_label p (globals p) s →
+cost_label_of_stmt … (sequential … s nxt) = None ?.
+#p * // #lbl#next *
+qed.
+
+let rec produce_trace_any_any
+  (p : evaluation_params)
+  (st : state_pc p) fd
+  (src : code_point p)
+  (b : list (joint_seq p (globals p))) on b :
+  ∀l : list (code_point p).
+  ∀dst : code_point p.
+  ∀st' : state p.
+  fetch_function p ? (ev_genv p) (pc … st) = return fd →
+  point_of_pointer p p (pc … st) = return src →
+  if list_not_empty ? b then
+    ! x ← stmt_at ?? (joint_if_code … fd) dst ; cost_label_of_stmt … x = None ?
+  else
+    True →
+  src ~❨b, l❩~> dst in joint_if_code … fd →
+  All ? (λx.bool_to_Prop (no_call_nor_label … x)) b →
+  repeat_eval_seq_no_pc p (io_env p) b st = return st' →
+  trace_any_any (joint_abstract_status p) st
+    (mk_state_pc ? st' (pointer_of_point ? p (pc ? st) dst)) ≝
+  match b
+  return λx.?→?→?→?→?→?→?→?→?→?
+  with
+  [ nil ⇒
+    λl,dst,st',fd_prf,src_prf,dst_prf,in_code,all_other,EQ1.
+    (taa_base (joint_abstract_status p) st)
+      ⌈trace_any_any (joint_abstract_status p) st st ↦
+       trace_any_any (joint_abstract_status p) st
+        (mk_state_pc ? st' (pointer_of_point ? p (pc ? st) dst))⌉
+  | cons hd tl ⇒
+    λl.
+    match l return λx.?→?→?→?→?→?→?→?→? with
+    [ nil ⇒ λdst,st',fd_prf,src_prf,dst_prf,in_code.⊥
+    | cons mid rest ⇒
+      λdst,st',fd_prf,src_prf,dst_prf,in_code,all_other,EQ1.
+      match io_evaluate ??? (io_env p st) (eval_seq_no_pc … (ev_genv p) st hd)
+      return λx.io_evaluate ??? (io_env p st) (eval_seq_no_pc … (ev_genv p) st hd) = x → ?
+      with
+      [ OK st_mid ⇒ λEQ2.
+        taa_step (joint_abstract_status p) st ?
+          (mk_state_pc ? st' (pointer_of_point ? p (pc ? st) dst)) ???
+          (produce_trace_any_any ?
+            (mk_state_pc ? st_mid (pointer_of_point ? p (pc ? st) mid))
+            fd mid tl rest dst ???????)
+      | Error _ ⇒ λEQ2.⊥
+      ] (refl …)
     ]
-  | ** [#lbl | #id #fd #args #dest ] #st'
-    #y * #EQ <EQ -y * normalize nodelta @rel_io_eq
-    whd in match succ_pc; normalize nodelta
-    >pc_pt >m_return_bind
-    letin src' ≝ (point_of_succ p src n) in H ⊢ %;
-    letin pc' ≝ (pointer_of_point p p … (pc ? st) src') #H
-    [>m_return_bind whd in match eval_step_flow; normalize nodelta
-     whd in match (pblock ?);
-     elim (goto … ge lbl st' ?)
-     [ #st'' >m_return_bind %
-     | #e %
-     ]
-    | normalize nodelta in IH ⊢ %; @(IH … tl_ok H)
-      [ @fetch_fn
-      | @point_of_pointer_of_point
+  ].
+  [ cases l in in_code; [2: #mid #rest *] normalize in ⊢ (%→?); #EQ
+    cases st in src_prf EQ1; -st #st #pc
+    #src_prf normalize in ⊢ (%→?); #EQ1 destruct
+    >(pointer_of_point_of_pointer … src_prf) %
+  | elim in_code
+  |12: lapply EQ1 whd in ⊢ (??%?→?);
+    >EQ2 normalize #ABS destruct(ABS)
+  |*:
+    elim in_code
+    * #nxt * #EQ3 #EQ4 #Hrest
+    elim all_other
+    #hd_other #tl_other
+    [ whd whd in match eval_state; normalize nodelta
+      >(fetch_statement_eq … fd_prf src_prf EQ3) >m_return_bind
+      whd in match eval_statement; normalize nodelta
+      whd in match eval_step; normalize nodelta
+      >m_bind_bind
+      >(no_call_nor_label_proceed … hd_other) >m_return_bind
+      >m_bind_bind
+      >io_evaluate_bind >EQ2 >m_return_bind
+      >m_return_bind
+      whd in match succ_pc; normalize nodelta
+      >m_bind_bind >src_prf >m_return_bind >m_return_bind
+      whd in match eval_step_flow; normalize nodelta
+      whd in ⊢ (??%%); >EQ4
+      >EQ2 %
+    | %{(sequential … hd nxt)} %{(fetch_statement_eq … fd_prf src_prf EQ3)}
+      cases all_other #hd_other #_
+      whd in match stmt_classifier; normalize nodelta
+      @no_call_nor_label_other assumption
+    | %* #H @H -H whd in ⊢ (??%?);
+      cases tl in Hrest tl_other;
+      [ cases rest [2: #hd' #tl' *] normalize in ⊢ (%→?); #EQ' destruct(EQ') *
+        lapply dst_prf
+        whd in match (as_pc_of ??);
+        whd in match fetch_statement; normalize nodelta
+        whd in match point_of_pointer; normalize nodelta
+        >point_of_offset_of_point
+        >m_return_bind
+        >fetch_function_from_block_eq
+        [ >fd_prf
+          >m_return_bind
+          cases (stmt_at ????)
+          [ #_ %
+          | #stmt #H @H
+          ]
+        | %
+        |
+        ]
+      | #hd' #tl' cases rest [*] #mid' #rest' * * #next' * #EQ5 #EQ6
+        #_ * #hd_other' #_
+        >fetch_statement_eq try assumption
+        [ @no_call_nor_label_uncosted assumption
+        | whd in match (as_pc_of ??);
+          whd in ⊢ (??%?);
+          >point_of_offset_of_point %
+        ]
       ]
+    | change with (! x ← ?;?) in EQ1 : (??%?);
+      >EQ2 in EQ1; #H @H
+    | assumption
+    | assumption
+    | cases (list_not_empty ??) [ assumption | % ]
+    | @point_of_pointer_of_point
+    | <fd_prf @fetch_function_from_block_eq %
     ]
   ]
-]
-qed.
-
-definition eval_block_cont_pc :
-  ∀globals.∀p : sem_params.∀ty.genv globals p →
-  state_pc p → block_cont p globals ty → stmt_type_if ? ty (code_point p) unit →
-  IO io_out io_in (bool × (state_pc p)) ≝
-  λglobals,p,ty,ge,st,b,nxt.
-  ! 〈flow, st'〉 ← eval_block_cont globals p ty ge st b ;
-  match ty return λx.stmt_type_if ? x ?? → stmt_type_if ? x ?? → ? with
-  [ SEQ ⇒ λflow,nxt.eval_step_flow ?? ge st'
-        (pointer_of_point ? p (pc ? st) nxt) flow
-  | FIN ⇒ λflow.λ_.
-    ! st' ← eval_fin_step_flow ?? ge st' (pblock … (pc ? st)) flow ;
-    return 〈true, st'〉
-  ] flow nxt.
-
-lemma eval_block_cont_in_code :
-  ∀p : sem_params.∀g,ty.∀ge : genv g p.∀st : state_pc p.∀fn,src,B,dst.
-  fetch_function … ge (pc … st) = OK … fn →
-  point_of_pointer ? p … (pc … st) = OK … src →
-  All ? (never_calls … ge) (\fst B) →
-  src ~❨B❩~> dst in joint_if_code … fn →
-  repeat_eval_state_flag (|B|) g p ge st =
-    eval_block_cont_pc g p ty ge st B dst.
-#p #g #ty #ge #st #fn #src * #l #s #dst #fetch_fn #pc_pt #l_ok
-* #mid * #l_in_code #s_in_code
-change with (1 + |l|) in match (|?|);
->commutative_plus
->repeat_eval_state_flag_plus
-change with (! x ← ? ; ?) in ⊢ (???%);
->m_bind_bind
->(eval_seq_list_in_code … fetch_fn pc_pt l_ok l_in_code)
->m_bind_bind
-@m_bind_ext_eq ** [#lbl | #id #fd #args #dest] #st'
-normalize nodelta
-[ -s_in_code lapply dst -dst cases ty
-  whd in match stmt_type_if; normalize nodelta
-  #dst >m_return_bind
-  [whd in match eval_step_flow; | whd in match eval_fin_step_flow; ]
-  normalize nodelta
-  whd in match (pblock ?);
-  elim (goto g p ge lbl st' ?) #x //
-| %
-| >m_return_bind normalize nodelta
-  >repeat_eval_state_flag_one
-  >m_bind_bind
-  lapply s_in_code -s_in_code lapply dst -dst lapply s -s cases ty
-  whd in match stmt_type_if; normalize nodelta
-  #s #dst [* #n * ] #s_in_code [ #n_is_dst ]
-  whd in match eval_state_flag; normalize nodelta
-  letin pc' ≝ (pointer_of_point p p (pc ? st) mid)
-  letin st_pc' ≝ (mk_state_pc ? st' pc')
-  >(fetch_statement_eq … ?? s_in_code)
-  [2,5: @point_of_pointer_of_point
-  |3,6: @fetch_fn
-  |*: >m_return_bind
-    whd in match eval_statement; normalize nodelta
-    @m_bind_ext_eq * #flow #st'' >m_return_bind [2:%]
-    whd in match succ_pc; normalize nodelta
-    >point_of_pointer_of_point >m_return_bind
-    >pointer_of_point_of_pointer [2: @refl |*:]
-    [ >point_of_pointer_of_point >n_is_dst %
-    | %
-    ]
-  ]
-]
-qed.
-     cases dst [*] #z @eval_tunnel assumption
-| cases dst [2: #z *]]
-* #mid * #tunn [#H | * #n * #H #G ]
-  elim (eval_tunnel … fetch_fn pc_pt tunn)
-  #n
-  letin st' ≝ (set_pc p (pointer_of_point p p (pc p st) mid) st)
-  #EQ1
-  cut (point_of_pointer ? p … (pc … st') = OK … mid)
-  [1,3: 
-    whd in match st'; >point_of_pointer_of_point % ] #pc_pt'
-  cut (fetch_function p … ge (pc … st') = OK … fn)
-  [1,3: >fetch_function_from_block_eq [1,4:@fetch_fn |*:] whd in match st';
-    @pointer_of_point_block] #fetch_fn'
-  [ %{(n + 1)} 
-  >repeat_eval_state_plus >EQ1 >m_return_bind
-  >repeat_eval_state_one change with (None ?) in match (! x ← None ? ; ?);
-  change with (! 〈flow,tr,st〉 ← ? ; ?) in match (eval_block_cont ??????);
-  change with (! s ← ? ; ?) in match (eval_state ????);
-  >(fetch_statement_eq … fetch_fn' pc_pt' H) >m_return_bind
-  >m_bind_bind
-  change with ( ! x ← ? ; ?) in match (eval_block_cont ???????);
-  cases s *
-  
-  @m_bind_ext_eq' ** #flow #tr1 #st1 normalize nodelta
-  >m_bind_bind change with st' in match (set_pc ???); @m_bind_ext_eq
-  change with (! fn ← ? ; ?) in match (fetch_statement ?????);
-  >m_bind_bind in ⊢ (??%?);
-  change with (pointer_of_point ????) in match (pc ??);
-  >point_of_pointer_of_point >m_return_bind
-  >(fetch_function_from_block_eq ???? (pc … st))
-  [2: @pointer_of_point_block ]
-  >fetch_fn >m_return_bind >H2 >m_return_bind
-  >m_bind_bind
-  change with (! x ← ? ; ?) in ⊢ (???%);
-  >fetch_fn n ⊢ (??(????%?)?); >m_return_bind
-  >(stmt_at_to_safe … src_prf) in ⊢ (??(????%?)?);
-  >H1 in ⊢ (??(????%?)?);
-  whd in ⊢ (??(λ_.???%));
-elim b
-[ #st #dst #fetch_fn #prf #through
-  #H elim (block_cont_to_tunnel … H) #dst'
-  * #EQdst >EQdst >m_return_bind #G
-  elim (eval_tunnel … fetch_fn prf … G) #x #EQ %{x}
-  >EQ %
-| 
-
- #dst #fetch_fn #prf #through
-lapply prf -prf lapply fetch_fn -fetch_fn
-lapply b -b lapply st -st
-elim through [2: #hd #tl #IH]
-[2:
-  
-#st * [1,4,7,10:|2,5,8,11:#s|3,6,9,12:#s#b'] #fetch_fn #prf
-normalize in ⊢(%→?);
-[8: #EQ1 |*: * [5: |*: *] #lbl [ |*: *] * #H1 #H2 [|*: #H3] #x [ *
-[ * || * | * #lbl
- * #lbl * [*] #H1 #H2 [#H3]
-  
-let rec block_cont_in_code (p : sem_params) g (b : block_cont p g)
-  (following : option (succ p)) (c : codeT p g) (at : cpointer) on b : Prop ≝
-  match b with
-  [ Skip ⇒
-    match following with
-    [ Some l ⇒ succ_pc p p 
-*)
+qed.

src/joint/semantics_paolo.ma

@@ -16 +16 @@
 definition xpointer ≝ Σp.ptype p = XData.
 unification hint 0 ≔ ⊢ cpointer ≡ Sig pointer (λp.ptype p = Code).
-unification hint 0 ≔ ⊢ xpointer ≡ Sig pointer (λp.ptype p = XData).
+unification hint 0 ≔ ⊢ xpointer ≡ Sig pointer   (λp.ptype p = XData).
 
 record sem_state_params : Type[1] ≝
@@ -86 +86 @@
  λpars,globals,ge,p.function_of_block pars globals ge (pblock p).
 
-inductive step_flow (p : params) (globals : list ident) (labels : list label) : Type[0] ≝
-  | Redirect : (Σl.In ? labels l) → step_flow p globals labels (* used for goto-like flow alteration *)
-  | Init     : Z → joint_internal_function globals p → call_args p → call_dest p → step_flow p globals labels (* call a function with given id, then proceed *)
-  | Proceed  : step_flow p globals labels. (* go to implicit successor *)
-
+inductive step_flow (p : params) (globals : list ident) : possible_flows → Type[0] ≝
+  | Redirect : ∀lbls.(Σl.In ? lbls l) → step_flow p globals (Labels lbls) (* used for goto-like flow alteration *)
+  | Init     : Z → joint_internal_function globals p → call_args p → call_dest p → step_flow p globals Call (* call a function with given id, then proceed *)
+  | Proceed  : ∀flows.step_flow p globals flows. (* go to implicit successor *)
+
+(*
 definition step_flow_cons : ∀p,globals,l,lbls.
   step_flow p globals lbls → step_flow p globals (l :: lbls) ≝
@@ -120 +121 @@
 coercion step_flow_r : ∀p,globals,l1,l2.∀flow : step_flow p globals l2.step_flow p globals (l1@l2) ≝
   step_flow_append_r on _flow : step_flow ??? to step_flow ?? (append ???).
-
-inductive fin_step_flow (p : params) (globals : list ident) (labels : list label): Type[0] ≝
-  | FRedirect : (Σl.In ? labels l) → fin_step_flow p globals labels
-  | FTailInit : Z → joint_internal_function globals p → call_args p → fin_step_flow p globals labels
-  | FEnd  : fin_step_flow p globals labels. (* end flow *)
-
+*)
+
+inductive fin_step_flow (p : params) (globals : list ident) : possible_flows → Type[0] ≝
+  | FRedirect : ∀lbls.(Σl.In ? lbls l) → fin_step_flow p globals (Labels lbls)
+  | FTailInit : Z → joint_internal_function globals p → call_args p → fin_step_flow p globals Call
+  | FEnd1  : fin_step_flow p globals (Labels [ ]) (* end flow *)
+  | FEnd2  : fin_step_flow p globals Call. (* end flow *)
+
+(*
 definition fin_step_flow_cons : ∀p,globals,l,lbls.
   fin_step_flow p globals lbls → fin_step_flow p globals (l :: lbls) ≝
@@ -155 +159 @@
 coercion fin_step_flow_r : ∀p,globals,l1,l2.∀flow : fin_step_flow p globals l2.fin_step_flow p globals (l1@l2) ≝
   fin_step_flow_append_r on _flow : fin_step_flow ??? to fin_step_flow ?? (append ???).
+*)
 
 record more_sem_unserialized_params (uns_pars : unserialized_params) : Type[1] ≝
@@ -230 +235 @@
    serialization and on whether the call is a tail one. *)
 definition eval_call_block:
- ∀globals.∀p : params.∀p':more_sem_unserialized_params p.∀lbls.
+ ∀globals.∀p : params.∀p':more_sem_unserialized_params p.
   genv globals p → state p' → block → call_args p → call_dest p →
-    IO io_out io_in ((step_flow p globals lbls)×(state p')) ≝
- λglobals,p,p',lbls,ge,st,b,args,dest.
+    IO io_out io_in ((step_flow p globals Call)×(state p')) ≝
+ λglobals,p,p',ge,st,b,args,dest.
   ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr … ge b) : IO ? io_in ?); 
     match fd with
@@ -258 +263 @@
   let isp'' ≝ shift_pointer … isp' [[false;false;false;false;false;false;false;true]] in
   return set_m … m (set_isp … isp'' st).
-  normalize elim (isp p st) //
+  normalize elim (isp p st) #p #H @H
 qed.
 
@@ -268 +273 @@
   do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp'');
   OK ? 〈ist,v〉.
-  normalize elim (isp p st) //
+  normalize elim (isp p st) #p #H @H
 qed.
   
@@ -290 +295 @@
   ; read_result: ∀globals.genv globals pp → state msu_pars → res (list beval)
   (* change of pc must be left to *_flow execution *)
-  ; exec_extended: ∀globals.genv globals pp → ∀s : ext_step pp.
+  ; eval_ext_seq: ∀globals.genv globals pp → ext_seq pp →
+      state msu_pars → IO io_out io_in (state msu_pars)
+  ; eval_ext_tailcall : ∀globals.genv globals pp → ext_tailcall pp →
+      state msu_pars → IO io_out io_in ((fin_step_flow pp globals Call)×(state msu_pars))
+  ; eval_ext_call: ∀globals.genv globals pp →∀s : ext_call pp.
       state msu_pars →
-      IO io_out io_in ((step_flow pp globals (ext_step_labels … s))× (state msu_pars))
-  ; exec_fin_extended: ∀globals.genv globals pp → ∀s : ext_fin_stmt pp.
-      state msu_pars →
-      IO io_out io_in ((fin_step_flow pp globals (ext_fin_stmt_labels … s))×(state msu_pars))
+      IO io_out io_in ((step_flow pp globals Call)×(state msu_pars))
   ; pop_frame: ∀globals.genv globals pp → state msu_pars → res (state msu_pars)
   }.
@@ -311 +317 @@
   cpointer→ code_point p → cpointer ≝
   λp,msp,ptr,pt.
-    mk_pointer Code (pblock ptr) ? (offset_of_point p msp pt).
-[ elim ptr #ptr' #EQ <EQ @pok
-| %] qed.
+    mk_pointer (pblock ptr) (offset_of_point p msp pt).
+elim ptr #ptr' #EQ <EQ % qed.
 
 axiom BadOffsetForCodePoint : String.
@@ -335 +340 @@
 lemma pointer_of_point_uses_block :
   ∀p,msp.∀ptr1,ptr2 : cpointer.∀pt.pblock ptr1 = pblock ptr2 → pointer_of_point p msp ptr1 pt = pointer_of_point p msp ptr2 pt.
-#p #msp ** #ty1 #bl1 #H1 #o1 #EQ1
-        ** #ty2 #bl2 #H2 #o2 #EQ2
+#p #msp ** #b1 #o1 #EQ1
+        ** #b2 #o2 #EQ2
 #pt #EQ3 destruct normalize //
 qed.
@@ -344 +349 @@
     pblock ptr1 = pblock ptr2 → point_of_pointer p msp ptr1 = OK … pt →
     pointer_of_point p msp ptr2 pt = ptr1.
-#p #msp ** #ty1 #bl1 #H1 #o1 #EQ1
-        ** #ty2 #bl2 #H2 #o2 #EQ2 #pt #EQ
+#p #msp ** #b1 #o1 #EQ1
+        ** #b2 #o2 #EQ2
+#pt #EQ3
 destruct
 lapply (offset_of_point_of_offset p msp o1)
@@ -365 +371 @@
   opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt).
   
-definition pointer_of_label_in_block : ∀p : params.∀ msp : more_sem_params p.∀globals.
-  genv globals p → block → label → res cpointer ≝
-  λp,msp,globals,ge,b,lbl.
-  ! fn ← function_of_block … ge b ;
+definition pointer_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals.
+  genv globals p → cpointer → label → res cpointer ≝
+  λp,msp,globals,ge,ptr,lbl.
+  ! fn ← fetch_function … ge ptr ;
   ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl]
             (point_of_label … (joint_if_code … fn) lbl) ;
-  return (mk_pointer Code (mk_block Code (block_id b)) ? (offset_of_point p msp pt) : Σp.?). // qed.
-
-definition pointer_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals.
-  genv globals p → cpointer → label → res cpointer ≝
-  λp,msp,globals,ge,ptr.
-  pointer_of_label_in_block p msp globals ge (pblock ptr).
+  return (mk_pointer(mk_block Code (block_id (pblock ptr)))
+    (offset_of_point p msp pt) : Σp.?). // qed.
 
 definition succ_pc : ∀p : params.∀ msp : more_sem_params p.
@@ -396 +398 @@
 
 definition goto: ∀globals. ∀p:sem_params.
-  genv globals p → label → state p → block → res (state_pc p) ≝
+  genv globals p → label → state p → cpointer → res (state_pc p) ≝
  λglobals,p,ge,l,st,b.
-  ! newpc ← pointer_of_label_in_block ? p … ge b l ;
+  ! newpc ← pointer_of_label ? p … ge b l ;
   return mk_state_pc ? st newpc.
 
@@ -416 +418 @@
 axiom SuccessorNotProvided : String.
 
-(* the optional point must be given only for calls *)
-definition eval_step :
+definition eval_seq_no_pc :
  ∀globals.∀p:sem_params. genv globals p → state p →
-  ∀s:joint_step p globals.
-  IO io_out io_in ((step_flow p globals (step_labels … s))×(state p)) ≝
+  ∀s:joint_seq p globals.
+  IO io_out io_in (state p) ≝
  λglobals,p,ge,st,seq.
-  match seq return λx.IO ?? ((step_flow ?? (step_labels … x) × ?)) with
-  [ extension c ⇒
-    exec_extended … ge c st
-  | COST_LABEL cl ⇒
-    return 〈Proceed ???, st〉
-  | COMMENT c ⇒
-    return 〈Proceed ???, st〉
+  match seq return λx.IO ??? with
+  [ extension_seq c ⇒
+    eval_ext_seq ??? ge c st
   | LOAD dst addrl addrh ⇒
     ! vaddrh ← dph_arg_retrieve … st addrh ;
@@ -434 +431 @@
     ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
     ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
-    ! st ← acca_store p … dst v st ;
-    return 〈Proceed ???, st〉
+    acca_store p … dst v st
   | STORE addrl addrh src ⇒
     ! vaddrh ← dph_arg_retrieve … st addrh;
@@ -442 +438 @@
     ! v ← acca_arg_retrieve … st src;
     ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
-    return 〈Proceed ???, set_m … m' st〉
-  | COND src ltrue ⇒
-    ! v ← acca_retrieve … st src;
-    ! b ← bool_of_beval v;
-    if b then
-      return 〈Redirect ??? ltrue, st〉
-    else
-      return 〈Proceed ???, st〉
+    return set_m … m' st
   | ADDRESS ident prf ldest hdest ⇒
     let addr ≝ opt_safe ? (find_symbol … ge ident) ? in
-    ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer (block_region addr) addr ? zero_offset) ;
+    ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer addr zero_offset) ;
     ! st' ← dpl_store … ldest laddr st;
-    ! st'' ← dph_store … hdest haddr st';
-    return 〈Proceed ???, st''〉
+    dph_store … hdest haddr st'
   | OP1 op dacc_a sacc_a ⇒
     ! v ← acca_retrieve … st sacc_a;
     ! v ← Byte_of_val v;
     let v' ≝ BVByte (op1 eval op v) in
-    ! st ← acca_store … dacc_a v' st;
-    return 〈Proceed ???, st〉
+    acca_store … dacc_a v' st
   | OP2 op dacc_a sacc_a src ⇒
     ! v1 ← acca_arg_retrieve … st sacc_a;
@@ -472 +459 @@
       let carry ≝ beval_of_bool carry in
     ! st' ← acca_store … dacc_a v' st;
-      let st'' ≝ set_carry … carry st' in
-    return 〈Proceed ???, st''〉
+    return set_carry … carry st'
   | CLEAR_CARRY ⇒
-    let st' ≝ set_carry … BVfalse st in
-    return 〈Proceed ???, st'〉
+    return set_carry … BVfalse st
   | SET_CARRY ⇒
-    let st' ≝ set_carry … BVtrue st in
-    return 〈Proceed ???, st'〉
+    return set_carry … BVtrue st
   | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
     ! v1 ← acca_arg_retrieve … st sacc_a_reg;
@@ -489 +473 @@
     let v2' ≝ BVByte v2' in
     ! st' ← acca_store … dacc_a_reg v1' st;
-    ! st'' ← accb_store … dacc_b_reg v2' st';
-    return 〈Proceed ???, st''〉
+    accb_store … dacc_b_reg v2' st'
   | POP dst ⇒
     ! 〈st',v〉 ← pop p st;
-    ! st'' ← acca_store p p dst v st';
-    return 〈Proceed ???, st''〉
+    acca_store p p dst v st'
   | PUSH src ⇒
     ! v ← acca_arg_retrieve … st src;
-    ! st ← push … st v;
-    return 〈Proceed ???, st〉
+    push … st v
   | MOVE dst_src ⇒
-    ! st ← pair_reg_move … st dst_src ;
-    return 〈Proceed ???, st〉
+    pair_reg_move … st dst_src
   | CALL_ID id args dest ⇒
     ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
-    eval_call_block … ge st b args dest
+    ! 〈flow, st'〉 ← eval_call_block … ge st b args dest ;
+    return st'
+  | extension_call s ⇒
+    !〈flow, st'〉 ← eval_ext_call ??? ge s st ;
+    return st'
+  | _ ⇒ return st
   ].
-  [ cases addr //
-  | (* TODO: to prove *)
-    elim daemon
-  | %1 %
-  ] qed.
-
-definition eval_fin_step : ∀globals: list ident.∀p:sem_params. genv globals p →
-  state p → ∀s : joint_fin_step … p globals.
-  IO io_out io_in ((fin_step_flow p globals (fin_step_labels … s))×(state p)) ≝
+  (* TODO: to prove *)
+  elim daemon
+  qed.
+
+definition eval_seq_pc :
+ ∀globals.∀p:sem_params. genv globals p → state p →
+  ∀s:joint_seq p globals.
+  IO io_out io_in (step_flow p globals (step_flows … s)) ≝
+  λg,p,ge,st,s.match s return λx : joint_seq ??.IO ?? (step_flow ?? (step_flows … x)) with
+  [ CALL_ID id args dest ⇒
+    ! b ← opt_to_res \ldots  [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
+    ! 〈flow, st'〉 ← eval_call_block … ge st b args dest ;
+    return flow
+  | extension_call s ⇒
+    !〈flow, st'〉 ← eval_ext_call ??? ge s st ;
+    return flow
+  | _ ⇒ return Proceed ???
+  ].
+
+definition eval_step :
+ ∀globals.∀p:sem_params. genv globals p → state p →
+  ∀s:joint_step p globals.
+  IO io_out io_in ((step_flow p globals (step_flows … s))×(state p)) ≝
+  λglobals,p,ge,st,s.
+  match s return λx.IO ?? ((step_flow ?? (step_flows … x))×?) with
+  [ step_seq s ⇒
+    ! flow ← eval_seq_pc ?? ge st s ;
+    ! st' ← eval_seq_no_pc ?? ge st s ;
+    return 〈flow,st'〉
+  | COND src ltrue ⇒
+    ! v ← acca_retrieve … st src;
+    ! b ← bool_of_beval v;
+    if b then
+      return 〈Redirect ??? ltrue, st〉
+    else
+      return 〈Proceed ???, st〉
+  ].
+  %1 % qed.
+
+definition eval_fin_step_no_pc : ∀globals: list ident.∀p:sem_params. genv globals p →
+  state p → ∀s : joint_fin_step p.
+  IO io_out io_in (state p) ≝
  λglobals,p,ge,st,s.
-  match s return λx.IO ?? ((fin_step_flow ?? (fin_step_labels … x)) × ?) with
-    [ GOTO l ⇒ return 〈FRedirect ??? l, st〉
-    | RETURN ⇒ return 〈FEnd ???, st〉
-    | extension_fin c ⇒ exec_fin_extended … ge c st
-    ]. %1 % qed.
-
+  match s return λx.IO ??? with
+    [ tailcall c ⇒
+      !〈flow,st'〉 ← eval_ext_tailcall ??? ge c st ;
+      return st'
+    | _ ⇒ return st
+    ].
+
+definition eval_fin_step_pc :
+ ∀globals.∀p:sem_params. genv globals p → state p →
+  ∀s:joint_fin_step p.
+  IO io_out io_in (fin_step_flow p globals (fin_step_flows … s)) ≝
+  λg,p,ge,st,s.
+  match s return λx.IO ?? (fin_step_flow ?? (fin_step_flows … x)) with
+  [ tailcall c ⇒
+    !〈flow,st'〉 ← eval_ext_tailcall ??? ge c st ;
+    return flow  
+  | GOTO l ⇒ return FRedirect … l
+  | RETURN ⇒ return FEnd1 ??
+  ]. %1 % qed.
 
 definition do_call : ∀globals: list ident.∀p:sem_params. genv globals p →
@@ -532 +563 @@
     let l' ≝ joint_if_entry … fn in
     let st' ≝ set_regs p regs st in
-    let pointer_in_fn ≝ mk_pointer Code (mk_block Code id) ? (mk_offset 0) in
+    let pointer_in_fn ≝ mk_pointer (mk_block Code id) (mk_offset (bv_zero …)) in
     let pc ≝ pointer_of_point ? p … pointer_in_fn l' in
     return mk_state_pc ? st' pc. % qed.
 
-(* The pointer provided is the one to the *next* instruction.
-   The boolean tells wether a flow changement has occurred (i.e.
-   a non Proceed cmd was issued). Used in linking block evaluation
-   with regular one *)
+(* The pointer provided is the one to the *next* instruction. *)
 definition eval_step_flow :
- ∀globals.∀p:sem_params.∀lbls.genv globals p →
-  state p → cpointer → step_flow p globals lbls →
-    res (bool × (state_pc p)) ≝
- λglobals,p,lbls,ge,st,nxt,cmd.
+ ∀globals.∀p:sem_params.∀flows.genv globals p →
+ state p → cpointer → step_flow p globals flows → res (state_pc p) ≝
+ λglobals,p,flows,ge,st,nxt,cmd.
  match cmd with
-  [ Redirect l ⇒
-    ! st ← goto … ge l st (pblock nxt) ; return 〈true, st〉
+  [ Redirect _ l ⇒
+    goto … ge l st nxt
   | Init id fn args dest ⇒
     let st' ≝ set_frms … (save_frame … nxt dest st) st in
-    ! st ← do_call ?? ge st' id fn args ;
-    return 〈true, st〉
-  | Proceed ⇒
-    return 〈false, mk_state_pc ? st nxt〉
+    do_call ?? ge st' id fn args
+  | Proceed _ ⇒
+    return mk_state_pc ? st nxt
   ].
 
-definition eval_fin_step_flow : ∀globals: list ident.∀p:sem_params.∀lbls. genv globals p →
-  state p → block → fin_step_flow p globals lbls → res (state_pc p) ≝
-  λglobals,p,lbls,ge,st,b,cmd.
+definition eval_fin_step_flow : ∀globals: list ident.∀p:sem_params.∀flows. genv globals p →
+  state p → cpointer → fin_step_flow p globals flows → res (state_pc p) ≝
+  λglobals,p,lbls,ge,st,curr,cmd.
   match cmd with
-  [ FRedirect l ⇒ goto … ge l st b
+  [ FRedirect _ l ⇒ goto … ge l st curr
   | FTailInit id fn args ⇒
     do_call … ge st id fn args
-  | FEnd ⇒
+  | _ ⇒
     ! 〈st',ra〉 ← fetch_ra … st ;
     ! st'' ← pop_frame … ge st;
@@ -572 +598 @@
  ∀globals.∀p:sem_params.genv globals p →
   state_pc p → joint_statement p globals →
-    IO io_out io_in (bool × (state_pc p)) ≝
+    IO io_out io_in (state_pc p) ≝
  λglobals,p,ge,st,stmt.
  match stmt with
  [ sequential s nxt ⇒
-   ! 〈flow, st'〉 ← eval_step … ge st s ;
+   ! 〈flow,st'〉 ← eval_step … ge st s ;
    ! nxtptr ← succ_pc ? p (pc … st) nxt ;
    eval_step_flow … ge st' nxtptr flow
  | final s ⇒
-   ! 〈flow, st'〉 ← eval_fin_step … ge st s ;
-   ! st ← eval_fin_step_flow … ge st' (pblock … (pc … st)) flow ;
-   return 〈true, st〉
+   ! st' ← eval_fin_step_no_pc … ge st s ;
+   ! flow ← eval_fin_step_pc … ge st s ;
+   eval_fin_step_flow … ge st' (pc … st) flow
  ].
 
-definition eval_state_flag : ∀globals: list ident.∀p:sem_params. genv globals p →
-  state_pc p → IO io_out io_in (bool × (state_pc p)) ≝
+definition eval_state : ∀globals: list ident.∀p:sem_params. genv globals p →
+  state_pc p → IO io_out io_in (state_pc p) ≝
   λglobals,p,ge,st.
   ! s ← fetch_statement ? p … ge (pc … st) : IO ???;
   eval_statement … ge st s.
-
-definition eval_state : ∀globals: list ident.∀p:sem_params. genv globals p →
-  state_pc p → IO io_out io_in (state_pc p) ≝
-  λglobals,p,ge,st.
-  ! 〈flag,st'〉 ← eval_state_flag … ge st ;
-  return st'.
 
 (* Paolo: what if in an intermediate language main finishes with an external
@@ -618 +638 @@
  | _ ⇒ Error ? [ ]
  ]).
- 
+
+(*
 record evaluation_parameters : Type[1] ≝
  { globals: list ident
@@ -681 +702 @@
  ∀pars:sem_params.fullexec io_out io_in ≝
  λpars.mk_fullexec ??? joint_exec (make_global pars) (make_initial_state pars).
+*)