Changeset 2592

Timestamp:

Jan 29, 2013, 11:20:53 AM (8 years ago)

Author:

piccolo

Message:

main lemma of ERTLptr in place

Location:

src

Files:

• ERTLptr/ERTLtoERTLptr.ma (modified) (1 diff)
• ERTLptr/ERTLtoERTLptrOK.ma (modified) (17 diffs)
• joint/semantics.ma (modified) (1 diff)

src/ERTLptr/ERTLtoERTLptr.ma

@@ -16 +16 @@
 include "ERTLptr/ERTLptr.ma".
 include "joint/TranslateUtils.ma".
-
+ 
 definition translate_step_seq :
 ∀globals.(joint_seq ERTL globals) → (joint_seq ERTLptr globals) ≝ 

src/ERTLptr/ERTLtoERTLptrOK.ma

@@ -46 +46 @@
     ERTLptr_semantics (pc_block pc) ertl_ptr_point.
 
-
 definition sigma_stored_pc ≝ 
 λprog,sigma,pc. match sigma_pc_opt prog sigma pc with
-      [None ⇒ null_pc | Some x ⇒ x].
+      [None ⇒ null_pc (pc_offset … pc) | Some x ⇒ x].
       
       
@@ -1088 +1087 @@
    
 definition dummy_state_pc : state_pc ERTL_semantics ≝ 
-mk_state_pc ? dummy_state null_pc null_pc.
+mk_state_pc ? dummy_state (null_pc one) (null_pc one).
 
 check fetch_internal_function
@@ -1684 +1683 @@
 qed.
 
+lemma sp_ok : ∀prog : ertl_program. ∀sigma : sigma_map (ertl_to_ertlptr prog).
+∀stack_size.
+∀fn : (joint_closed_internal_function ? (globals (mk_prog_params ERTL_semantics prog stack_size))).
+preserving1 … res_preserve1 …
+      (λst.sigma_state (ertl_to_ertlptr prog) sigma st (joint_if_locals ERTL ? fn))
+      (λx.x)
+      (sp ERTL_semantics)
+      (sp ERTLptr_semantics).
+cases daemon
+qed.
+
+lemma set_sp_ok :  ∀prog : ertl_program. 
+let trans_prog ≝ ertl_to_ertlptr prog in
+∀sigma : sigma_map trans_prog.
+∀stack_size.
+∀fn : (joint_closed_internal_function ? (globals (mk_prog_params ERTL_semantics prog stack_size))).
+∀ptr,st.
+set_sp ? ptr (sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn)) =
+sigma_state trans_prog sigma (set_sp ? ptr st) (joint_if_locals ERTL ? fn).
+cases daemon
+qed.
+
 lemma eval_seq_no_pc_no_call_ok :
 ∀prog : ertl_program.
@@ -1692 +1713 @@
       (λst.sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn))
       (λst.sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn))
-      (eval_seq_no_pc (mk_prog_params ERTL_semantics prog stack_size)
+      (eval_seq_no_pc ERTL_semantics
              (globals (mk_prog_params ERTL_semantics prog stack_size))
              (ev_genv (mk_prog_params ERTL_semantics prog stack_size)) id fn seq)
-      (eval_seq_no_pc (mk_prog_params ERTLptr_semantics trans_prog stack_size)
+      (eval_seq_no_pc ERTLptr_semantics
   (globals (mk_prog_params ERTLptr_semantics trans_prog stack_size))
   (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_size)) id (translate_internal … fn) (translate_step_seq … seq)).
@@ -1706 +1727 @@
   [ @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn))
   | change with (ertl_eval_move ??) in ⊢ (???????%%); @ertl_eval_move_ok
-  | #regs #st whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] % |]
+  | #regs  @mfr_return_eq1 % 
   ]
 | #r #st @mfr_bind1
@@ -1716 +1737 @@
     [@(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn))
     | @ps_reg_store_ok
-    | #regs #x whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] % |]
+    | #regs  @mfr_return_eq1 % 
     ]
   ]
@@ -1742 +1763 @@
                                                in ⊢ (???????(?????%?)?); 
        @ps_reg_store_ok
-    | #regs #st1 whd in match set_regs; whd in match sigma_state; normalize nodelta;
-      whd in ⊢(??%% → ?); #EQ destruct % [2: % [%] %|]
+    | #regs  @mfr_return_eq1 %
     ]
   | #st1 @opt_safe_elim #bl #EQbl @opt_safe_elim #bl'   
@@ -1754 +1774 @@
                                                in ⊢ (???????(?????%?)?); 
       @ps_reg_store_ok
-    | #regs #st1 whd in match set_regs; whd in match sigma_state; normalize nodelta;
-      whd in ⊢(??%% → ?); #EQ destruct % [2: % [%] %|]
+    | #regs  @mfr_return_eq1 % 
     ]
   ] 
@@ -1776 +1795 @@
          [  @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn))
          | @ps_reg_store_ok
-         | #regs #st1 whd in match set_regs; whd in match sigma_state; normalize nodelta;
-            whd in ⊢(??%% → ?); #EQ destruct % [2: % [%] %|]
+         | #regs  @mfr_return_eq1 % 
          ]
        | #st1 whd in match accb_store; normalize nodelta @mfr_bind1
@@ -1783 +1801 @@
          |  whd in match sigma_state; normalize nodelta
             @ps_reg_store_ok
-         | #regs #st1 whd in match set_regs; whd in match sigma_state; normalize nodelta;
-            whd in ⊢(??%% → ?); #EQ destruct % [2: % [%] %|]
-         ]
+         | #regs  @mfr_return_eq1 %         ]
        ]
      ]
@@ -1799 +1815 @@
       [ @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn))
       | whd in match sigma_state; normalize nodelta @ps_reg_store_ok
-      | #regs #st1 whd in match set_regs; whd in match sigma_state; normalize nodelta;
-            whd in ⊢(??%% → ?); #EQ destruct % [2: % [%] %|]
+      | #regs  @mfr_return_eq1 %
       ]
     ]
@@ -1818 +1833 @@
           [  @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn))
           | whd in match sigma_state; normalize nodelta @ps_reg_store_ok
-          | #regs #st1 whd in match set_regs; whd in match sigma_state; normalize nodelta;
-            whd in ⊢(??%% → ?); #EQ destruct % [2: % [%] %|]
+          | #regs  @mfr_return_eq1 %
           ]
-        | #st1 #st2 whd in match set_carry; whd in match sigma_state; normalize nodelta
-           whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] % |]  
+        | #st1 @mfr_return_eq1 %
         ]
       ]
     ]
   ]
-| #st whd in match set_carry; whd in match sigma_state; normalize nodelta
-  #st1 whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] % |]
-| #st #st1 whd in match set_carry; whd in match sigma_state; normalize nodelta
-   whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] % |]
+| #st  @mfr_return_eq1 %
+| #st  @mfr_return_eq1 % 
 | #r1 #dpl #dph #st @mfr_bind1
   [ @(sigma_beval (ertl_to_ertlptr prog) sigma)
@@ -1846 +1857 @@
           [ @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn))
           |  whd in match sigma_state; normalize nodelta @ps_reg_store_ok
-          | #regs #st1 whd in match set_regs; whd in match sigma_state; normalize nodelta;
-            whd in ⊢(??%% → ?); #EQ destruct % [2: % [%] %|]
+          | #regs  @mfr_return_eq1 %
           ]
         ]  
@@ -1868 +1878 @@
           [ @(sigma_mem (ertl_to_ertlptr prog) sigma)
           | @opt_to_res_preserve1 @bestorev_ok
-          | #m #st1 whd in ⊢ (??%% → ?); whd in match set_m; whd in match sigma_state;
-            normalize nodelta #EQ destruct % [2: % [%] %|]
+          | #m @mfr_return_eq1 %
           ]
         ]
@@ -1875 +1884 @@
     ]
   ]
-| #ext #st cases daemon
+| #ext #st whd in ⊢ (???????%%); whd in match (stack_sizes ????); cases (stack_size f)
+  normalize nodelta
+  [ @res_preserve_error1
+  | #n cases ext normalize nodelta
+    [1,2: @mfr_bind1
+      [1,4: @(λx.x)
+      |2,5: @sp_ok
+      |3,6: #ptr @mfr_return_eq1 >set_sp_ok %
+      ]
+    | #r whd in match ps_reg_store_status; normalize nodelta @mfr_bind1
+      [2: whd in match sigma_state; normalize nodelta
+          change with (sigma_beval ? sigma (BVByte ?)) in ⊢ (???????(??%?)?);
+          @ps_reg_store_ok
+      |
+      | #regs @mfr_return_eq1 %
+      ]
+    ]
+  ]      
 ]
 qed.
+
+lemma fetch_statement_commute :
+∀prog : ertl_program.
+let trans_prog ≝ (ertl_to_ertlptr prog) in
+∀sigma : sigma_map trans_prog.
+∀stack_sizes,id,fn,stmt,pc.
+fetch_statement ERTL_semantics 
+(globals (mk_prog_params ERTL_semantics prog stack_sizes))
+(ev_genv (mk_prog_params ERTL_semantics prog stack_sizes))
+pc = return 〈id,fn,stmt〉 → 
+match stmt with 
+[ sequential seq nxt ⇒
+    match seq with
+    [ CALL ids args dest ⇒
+        match ids with
+        [ inl i ⇒ 
+          fetch_statement ERTLptr_semantics 
+          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
+          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
+          pc = 
+          return 〈id,
+          translate_internal … fn,
+          sequential ?? (CALL ERTLptr ? (inl ?? i) args dest) nxt〉
+        | inr p ⇒ ?(*
+          ∃reg,lbl.
+          fetch_statement ERTLptr_semantics 
+          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
+          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
+           pc = return 〈id,translate_internal … fn,sequential ?? (extension_seq ERTLptr ? (LOW_ADDRESS reg lbl)) nxt〉
+           ∧ ∃ nxt'.
+           ! pc' ← get_pc_from_label ? ? (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
+                 id nxt;
+           fetch_statement ERTLptr_semantics 
+          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
+          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
+           pc' = return 〈id,translate_internal … fn,sequential ?? (step_seq ERTLptr ? (PUSH … (Reg … reg))) nxt'〉
+           ∧ ∃ nxt''.
+           ! pc' ← get_pc_from_label ? ? (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
+                 id nxt';
+           fetch_statement ERTLptr_semantics 
+          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
+          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
+           pc' = return 〈id,translate_internal … fn,sequential ?? (extension_seq ERTLptr ? (HIGH_ADDRESS reg lbl)) nxt''〉
+           ∧ ∃ nxt'''.
+           ! pc' ← get_pc_from_label ? ? (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
+                 id nxt'';
+           fetch_statement ERTLptr_semantics 
+          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
+          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
+           pc' = return 〈id,translate_internal … fn,sequential ?? (step_seq ERTLptr ? (PUSH … (Reg … reg))) nxt'''〉
+           ∧ ∃ nxt''''.
+           ! pc' ← get_pc_from_label ? ? (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
+                 id nxt''';
+           fetch_statement ERTLptr_semantics 
+          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
+          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
+           pc' = return 〈id,translate_internal … fn,sequential ?? (CALL ERTLptr ? (inr ?? p) args dest) nxt''''〉
+           ∧ sigma (translate_internal … fn) nxt''' =  return point_of_pc ERTL_semantics pc *)
+        ]
+    | COND r lbl ⇒ 
+          fetch_statement ERTLptr_semantics 
+          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
+          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
+          pc = 
+          return 〈id,
+          translate_internal … fn,
+          sequential ?? (COND ERTLptr ? r lbl) nxt〉
+    | step_seq s ⇒ 
+          fetch_statement ERTLptr_semantics 
+          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
+          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
+          pc = 
+          return 〈id,
+          translate_internal … fn,
+          sequential ?? (step_seq ERTLptr … (translate_step_seq ? s)) nxt〉
+    ]                   
+| final fin ⇒ 
+     fetch_statement ERTLptr_semantics 
+     (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
+     (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
+     pc = return 〈id,(translate_internal … fn),final … (joint_fin_step_id fin)〉
+| FCOND abs _ _ _ ⇒ Ⓧabs
+].
+cases daemon
+qed.
+
+lemma eval_seq_no_call_ok :
+ ∀prog.
+ let trans_prog ≝ ertl_to_ertlptr prog in
+ ∀sigma : sigma_map trans_prog.∀stack_sizes.
+ (*? →*) 
+ ∀st,st',f,fn,stmt,nxt.
+   fetch_statement ERTL_semantics 
+     (prog_var_names (joint_function ERTL_semantics) ℕ prog)
+    (ev_genv (mk_prog_params ERTL_semantics prog stack_sizes)) 
+    (pc … (sigma_state_pc ? sigma st)) =
+      return 〈f, fn,  sequential … (step_seq ERTL … stmt) nxt〉 →
+   eval_state ERTL_semantics
+   (prog_var_names (joint_function ERTL_semantics) ℕ prog) 
+   (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes)) 
+   (sigma_state_pc ? sigma st) =
+    return st' → 
+ ∃st''. st' = sigma_state_pc ? sigma st'' ∧
+ ∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes)
+  st
+  st''.
+ bool_to_Prop (taaf_non_empty … taf).
+#prog #sigma #stack_size #st1 #st2 #f #fn #stmt #nxt #EQf whd in match eval_state;
+normalize nodelta >EQf >m_return_bind whd in match eval_statement_advance; 
+whd in match eval_statement_no_pc; normalize nodelta
+ #H @('bind_inversion H) -H #st_no_pc #EQ lapply(err_eq_from_io ????? EQ) -EQ 
+#EQeval whd in ⊢ (??%% → ?); #EQ destruct lapply EQf 
+whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta @if_elim
+[ #EQbl
+| #pc_st1_spec inversion(fetch_internal_function ???) [2: #e #_]
+]
+[1,2: whd in match dummy_state_pc; whd in match null_pc; 
+  whd in match fetch_statement; normalize nodelta whd in match fetch_internal_function;
+  normalize nodelta lapply(fetch_function_no_zero ??????) 
+  [2,9: @( «mk_block Code OZ,refl region Code»)
+    |1,8: % |3,10: @prog |7,14: #EQ >EQ |*:]  whd in ⊢ (??%% → ?); #EQ destruct]
+* #f1 #fn1 #EQ lapply(jmeq_to_eq ??? EQ) -EQ #fn1_spec normalize nodelta
+whd in match fetch_statement; normalize nodelta >fn1_spec
+>m_return_bind #H @('bind_inversion H) -H #stmt1 #EQ 
+lapply(opt_eq_from_res ???? EQ) -EQ #stmt1_spec whd in ⊢ (??%% → ?); #EQ destruct
+lapply EQeval -EQeval whd in match sigma_state_pc in ⊢ (% → ?);
+normalize nodelta @if_elim [#H >H in pc_st1_spec; *] #_ >fn1_spec
+normalize nodelta #EQeval cases(eval_seq_no_pc_no_call_ok ???????? EQeval)
+#st_no_pc' * #EQeval' #EQst_no_pc' 
+whd in match set_no_pc; normalize nodelta 
+% [ % [@st_no_pc'|@(succ_pc ERTL_semantics (pc ERTL_semantics (sigma_state_pc prog sigma st1))
+   nxt)| @(last_pop ? st1)]]
+% [ whd in match sigma_state_pc; normalize nodelta
+    @if_elim [#H >H in pc_st1_spec; *] #_ >fn1_spec normalize nodelta 
+    @if_elim [#H >H in pc_st1_spec; *] #_ >fn1_spec normalize nodelta
+    >EQst_no_pc' %]
+%{(taaf_step … (taa_base …) …)} 
+[3: //] lapply(fetch_statement_commute ? sigma ????? EQf) normalize nodelta
+whd in match sigma_state_pc; normalize nodelta
+@if_elim [1,3:#H >H in pc_st1_spec; *] #_ >fn1_spec normalize nodelta
+#EQf1
+[ whd in match as_classifier; normalize nodelta whd in match (as_classify ??);
+  >EQf1 normalize nodelta %
+| whd in match (as_execute ???); whd in match eval_state; normalize nodelta
+  >EQf1 >m_return_bind whd in match eval_statement_no_pc; normalize nodelta
+  >EQeval' >m_return_bind %
+]
+qed.
+
+lemma pc_of_label_eq :
+  ∀globals,ge,bl,i_fn,lbl.
+  fetch_internal_function ? ge bl = return i_fn →
+  pc_of_label ERTL_semantics globals ge bl lbl =
+    OK ? (pc_of_point ERTL_semantics bl lbl).
+#globals #ge #bl #i_fn #lbl #EQf whd in match pc_of_label;
+normalize nodelta >EQf %
+qed.
+
+lemma eval_goto_ok :
+ ∀prog : ertl_program.
+ let trans_prog ≝ ertl_to_ertlptr prog in
+ ∀stack_sizes.
+ ∀sigma : sigma_map trans_prog.
+ ∀st,st',f,fn,nxt.
+   fetch_statement ERTL_semantics …
+    (globalenv_noinit ? prog) (pc … (sigma_state_pc ? sigma st)) =
+      return 〈f, fn,  final … (GOTO ERTL … nxt)〉 → 
+   eval_state ERTL_semantics
+   (prog_var_names (joint_function ERTL_semantics) ℕ prog) 
+   (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes)) 
+   (sigma_state_pc ? sigma st) =
+    return st' → 
+    ∃ st''. st' = sigma_state_pc ? sigma st'' ∧
+ ∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes)
+  st
+  st''.
+ bool_to_Prop (taaf_non_empty … taf).
+#prog #stack_sizes #sigma #st #st' #f #fn #nxt
+whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta
+@if_elim 
+[ #EQbl whd in match dummy_state_pc; whd in match null_pc;
+  whd in match fetch_statement; whd in match fetch_internal_function;
+  normalize nodelta lapply(fetch_function_no_zero ??????) 
+  [2: @( «mk_block Code OZ,refl region Code»)
+    | % | @prog |7: #EQ >EQ |*:]  whd in ⊢ (??%% → ?); #EQ destruct]
+#Hbl inversion(fetch_internal_function ???)
+[2: #e #_ normalize nodelta whd in match dummy_state_pc; whd in match null_pc;
+   whd in match fetch_statement; whd in match fetch_internal_function;
+  normalize nodelta lapply(fetch_function_no_zero ??????) 
+  [2: @( «mk_block Code OZ,refl region Code»)
+    | % | @prog |7: #EQ >EQ |*:]  whd in ⊢ (??%% → ?); #EQ destruct]
+* #f1 #fn1 #EQ lapply(jmeq_to_eq ??? EQ) -EQ #fn1_spec normalize nodelta
+#EQf lapply EQf whd in match fetch_statement; normalize nodelta >fn1_spec
+>m_return_bind #H @('bind_inversion H) -H #stmt' #_ whd in ⊢ (??%% → ?);
+#EQ destruct whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta
+@if_elim [#H >H in Hbl; *] #_ >fn1_spec normalize nodelta whd in match eval_state;
+normalize nodelta >EQf >m_return_bind whd in match eval_statement_advance; 
+whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
+whd in match goto; normalize nodelta #H lapply (err_eq_from_io ????? H) -H
+#H @('bind_inversion H) -H #pc' whd in match set_no_pc; normalize nodelta
+>(pc_of_label_eq … fn1_spec) whd in ⊢ (???% → ?); #EQ whd in ⊢ (??%% → ?); #EQ1 
+destruct lapply (fetch_statement_commute … sigma … stack_sizes … EQf)
+normalize nodelta #EQf' % 
+[ % [ @st 
+    | @(mk_program_counter 
+         (pc_block (pc ERTLptr_semantics st))
+         (offset_of_point ERTL_semantics nxt)) 
+    | @(last_pop … st)
+    ]
+] % 
+[ whd in match sigma_state_pc; normalize nodelta @if_elim [#H >H in Hbl; *]
+  >fn1_spec normalize nodelta #_ % ] 
+%{(taaf_step … (taa_base …) …)}
+[ whd in match as_classifier; normalize nodelta whd in match (as_classify ??);
+  >EQf' normalize nodelta %
+| whd in match (as_execute ???); whd in match eval_state; normalize nodelta
+  >EQf' >m_return_bind whd in match eval_statement_no_pc; 
+  whd in match eval_statement_advance; normalize nodelta >m_return_bind
+  whd in match goto; normalize nodelta whd in match pc_of_label; normalize nodelta
+  lapply(fetch_internal_function_transf ??????? fn1_spec)
+  [ #vars @translate_internal |] #EQ >EQ >m_return_bind %
+| %
+]
+qed.
+
+axiom partial_inj_sigma : ∀ prog : ertlptr_program.
+∀sigma :sigma_map prog. 
+∀fn,lbl1,lbl2. sigma fn lbl1 ≠ None ? → sigma fn lbl1 = sigma fn lbl2 → lbl1 = lbl2.
+
+lemma pop_ra_ok : 
+∀prog : ertl_program.
+let trans_prog ≝ ertl_to_ertlptr prog in
+∀sigma : sigma_map trans_prog. 
+∀stack_size.
+∀fn : (joint_closed_internal_function ? (globals (mk_prog_params ERTL_semantics prog stack_size))).
+preserving1 … res_preserve1 …
+     (λst.sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn))
+     (λx.let 〈st,pc〉 ≝ x in 
+       〈sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn),
+        sigma_stored_pc ? sigma pc〉)
+     (pop_ra ERTL_semantics)
+     (pop_ra ERTLptr_semantics).
+#prog #sigma #stack_size #fn #st whd in match pop_ra; normalize nodelta @mfr_bind1
+[ | @pop_ok ] * #bv #st1 @mfr_bind1 [ | @pop_ok] * #bv1 #st2 @mfr_bind1
+[ @(sigma_stored_pc ? sigma) | whd in match pc_of_bevals; normalize nodelta 
+  cases bv [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p]
+  whd in match sigma_beval; normalize nodelta try @res_preserve_error1
+  inversion(sigma_pc_opt ? ? ?) normalize nodelta [ #_ @res_preserve_error1]
+  #sigma_pc #sigma_pc_spec normalize nodelta cases bv1
+  [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
+  normalize nodelta try @res_preserve_error1 
+  inversion(sigma_pc_opt ? ? ?) normalize nodelta [#_ @res_preserve_error1]
+  #sigma_pc1 #sigma_pc1_spec @if_elim [2: #_ @res_preserve_error1]
+  @andb_elim @if_elim [2: #_ *] @andb_elim @if_elim [2: #_ *]
+  #_ #H >H @eq_program_counter_elim [2: #_ *]
+  #EQspc * @eq_program_counter_elim 
+  [#_ normalize nodelta @mfr_return_eq1 whd in match sigma_stored_pc; normalize nodelta
+   >sigma_pc1_spec %] * #H1 @⊥ @H1 >EQspc in sigma_pc_spec; <sigma_pc1_spec
+   whd in match sigma_pc_opt; normalize nodelta @if_elim
+  [ #H2 #EQ lapply(sym_eq ??? EQ) -EQ @if_elim [#_  whd in ⊢ (??%% → ?); #EQ destruct %]
+    #H3 #H @('bind_inversion H) -H #x #_ #H @('bind_inversion H) -H #y #_
+    cases sigma_pc1 in H2; #bl_pc1 #z #H2 whd in ⊢ (??%? → ?); #EQ destruct >H2 in H3; *
+  | #H2 @if_elim 
+    [ #H3 #H @('bind_inversion H) -H #x1 #_ #H @('bind_inversion H) -H #lbl1 #_
+      cases pc in H2; #bl #z #H2 whd in match pc_of_point; normalize nodelta whd in ⊢ (??%? → ?);
+      #EQ destruct >H3 in H2; *
+    | #H3 lapply sigma_pc1_spec; whd in match sigma_pc_opt; normalize nodelta @if_elim
+     [#H >H in H3; *] #_ #EQ >EQ @('bind_inversion EQ) -EQ #x #x_spec 
+     lapply(res_eq_from_opt ??? x_spec) -x_spec #x_spec #H @('bind_inversion H) * #lbl 
+     #lbl_spec whd in match pc_of_point; normalize nodelta cases sigma_pc1 #bl1 #lbl1
+     whd in match (offset_of_point ??); whd in ⊢ (??%? → ?); #EQ destruct cases pc #bl2 #p2 
+     #H @('bind_inversion H) -H #x1 #x1_spec lapply(res_eq_from_opt ??? x1_spec) -x1_spec #x1_spec
+     #H @('bind_inversion H) -H * #lbl2 #lbl2_spec
+     whd in match (offset_of_point ??); whd in ⊢ (??%? → ?); #EQ destruct
+     <lbl_spec in lbl2_spec; #EQsig >x_spec in x1_spec; whd in ⊢ (??%% → ?); #EQ destruct
+     lapply(partial_inj_sigma (ertl_to_ertlptr prog) sigma ???? EQsig)
+     [>EQsig >lbl_spec % #ABS destruct] whd in match point_of_pc; normalize nodelta
+     whd in match (point_of_offset ??); whd in match (point_of_offset ??);
+     #EQ destruct cases pc1 #bl #p %
+    ]
+  ]
+| #pc @mfr_return_eq1 %
+]
+qed. 
+
+lemma pc_block_eq : ∀prog : ertl_program.
+let trans_prog ≝ ertl_to_ertlptr prog in
+∀sigma : sigma_map trans_prog.
+∀pc,id,fn.
+fetch_internal_function (joint_closed_internal_function ERTLptr
+  (prog_var_names (joint_function ERTLptr) ℕ trans_prog))
+  (globalenv_noinit (joint_function ERTLptr) trans_prog) (pc_block … pc) = return 〈id,fn〉→ 
+sigma fn (point_of_pc ERTL_semantics pc) ≠ None ? → 
+ pc_block … pc = pc_block … (sigma_stored_pc trans_prog sigma pc).
+#prog #sigma * #bl #pos #id #fn #EQfn #EQlbl whd in match sigma_stored_pc; 
+normalize nodelta whd in match sigma_pc_opt; normalize nodelta @if_elim [ #_ %]
+#_ >EQfn >m_return_bind >(opt_to_opt_safe … EQlbl) >m_return_bind %
+qed.
+                        
+
+ 
+lemma eval_return_ok :
+∀prog : ertl_program.
+let trans_prog ≝ ertl_to_ertlptr prog in
+∀stack_sizes.
+∀sigma : sigma_map trans_prog.
+∀st,st',f,fn.
+ fetch_statement ERTL_semantics …
+  (globalenv_noinit ? prog) (pc … (sigma_state_pc ? sigma st)) =
+    return 〈f, fn,  final … (RETURN ERTL … )〉 → 
+ eval_state ERTL_semantics
+   (prog_var_names (joint_function ERTL_semantics) ℕ prog) 
+   (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes)) 
+   (sigma_state_pc ? sigma st) =
+  return st' →
+joint_classify (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)
+  st = Some ? cl_return ∧
+∃ st''. st' = sigma_state_pc ? sigma st'' ∧
+∃st2_after_ret.
+∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes)
+st2_after_ret
+st''.
+(if taaf_non_empty … taf then
+  ¬as_costed (ERTLptr_status trans_prog stack_sizes)
+    st2_after_ret
+ else True) ∧
+eval_state … (ev_genv …  (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) st =
+return st2_after_ret ∧ 
+ret_rel ?? (ERTLptrStatusSimulation prog stack_sizes sigma) st' st2_after_ret.
+#prog #stack_size #sigma #st #st' #f #fn
+whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta
+@if_elim 
+[ #EQbl whd in match dummy_state_pc; whd in match null_pc;
+  whd in match fetch_statement; whd in match fetch_internal_function;
+  normalize nodelta lapply(fetch_function_no_zero ??????) 
+  [2: @( «mk_block Code OZ,refl region Code»)
+    | % | @prog |7: #EQ >EQ |*:]  whd in ⊢ (??%% → ?); #EQ destruct]
+#Hbl inversion(fetch_internal_function ???)
+[2: #e #_ normalize nodelta whd in match dummy_state_pc; whd in match null_pc;
+   whd in match fetch_statement; whd in match fetch_internal_function;
+  normalize nodelta lapply(fetch_function_no_zero ??????) 
+  [2: @( «mk_block Code OZ,refl region Code»)
+    | % | @prog |7: #EQ >EQ |*:]  whd in ⊢ (??%% → ?); #EQ destruct]
+* #f1 #fn1 #EQ lapply(jmeq_to_eq ??? EQ) -EQ #fn1_spec normalize nodelta
+#EQf lapply EQf whd in match fetch_statement; normalize nodelta >fn1_spec
+>m_return_bind #H @('bind_inversion H) -H #stmt' #_ whd in ⊢ (??%% → ?);
+#EQ destruct whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta
+@if_elim [#H >H in Hbl; *] #_ >fn1_spec normalize nodelta
+whd in match eval_state; normalize nodelta >EQf >m_return_bind
+whd in match eval_statement_no_pc; whd in match eval_statement_advance;
+normalize nodelta >m_return_bind
+#H lapply (err_eq_from_io ????? H) -H #H @('bind_inversion H) -H 
+* #st1 #pc1 #EQpop whd in match next_of_call_pc; normalize nodelta
+>m_bind_bind #H @('bind_inversion H) -H ** #f1 #fn2 * normalize nodelta
+[ * [ #c_id #args #dest | #r #lbl | #seq ] #nxt | #fin | * ]
+#EQf1 normalize nodelta [2,3,4: whd in ⊢ (??%% → ?); #EQ destruct]
+>m_return_bind whd in ⊢ (??%% → ?); #EQ destruct
+lapply (fetch_statement_commute prog sigma stack_size … EQf)
+normalize nodelta #EQf'
+% [ whd in match joint_classify; normalize nodelta >EQf' >m_return_bind %]
+cases(pop_ra_ok ? sigma  stack_size ??? EQpop) * #st3 #pc3 * #st3_spec
+normalize nodelta #EQ destruct whd in match set_last_pop; whd in match succ_pc; 
+normalize nodelta whd in match (point_of_succ ???);
+ % [ % [ @st3 | @(pc_of_point ERTL_semantics (pc_block … pc3) nxt) | @pc3] ] 
+ % [  @('bind_inversion EQf1) * #f3 #fn3 whd in match sigma_stored_pc;
+      normalize nodelta inversion(sigma_pc_opt ???) normalize nodelta
+      [ #_ #H @('bind_inversion H) -H #x whd in match null_pc; normalize nodelta
+        >fetch_function_no_zero [2: %] whd in ⊢ (???% → ?); #EQ destruct
+      | #pc4 whd in match sigma_pc_opt; normalize nodelta @if_elim
+        [ #bl3_spec @('bind_inversion EQf1) #x #H @('bind_inversion H) -H
+          #x1 >fetch_function_no_minus_one [ whd in ⊢ (???% → ?); #EQ destruct] 
+          lapply bl3_spec @eqZb_elim #EQ * whd in match sigma_stored_pc;
+          normalize nodelta whd in match sigma_pc_opt; normalize nodelta
+           >bl3_spec normalize nodelta assumption
+        | #bl3_spec #H @('bind_inversion H) -H * #fn4 #id4 
+          #H lapply(res_eq_from_opt ??? H) -H #fn4_spec
+          #H @('bind_inversion H) -H #lbl4 #lbl4_spec whd in ⊢ (??%? → ?); #EQ
+          destruct #fn3_spec #H @('bind_inversion H) -H #stmt1 #_ 
+          whd in ⊢ (??%% → ?); #EQ destruct 
+          >(fetch_internal_function_transf … fn3_spec) in fn4_spec; 
+          whd in ⊢ (??%% → ?); #EQ destruct
+        ]
+      ]
+      whd in match sigma_state_pc; normalize nodelta @if_elim
+      [ >(pc_block_eq prog sigma ????) in bl3_spec; 
+       [2: >lbl4_spec % #ABS destruct 
+       |3: >(fetch_internal_function_transf … fn3_spec) % |*:]
+       #bl3_spec whd in match pc_of_point; normalize nodelta #EQ >EQ in bl3_spec; *
+      | #_ inversion(fetch_internal_function ???) [#x #_ normalize nodelta % cases daemon (*serve lemma sul fetch della call *)
+        xxxxxxxxxxxxxxx
+            |
+ whd in match sigma_state_pc; normalize nodelta @if_elim
+   
+qed. 
+
+lemma eval_tailcall_ok :
+∀prog.
+let trans_prog ≝ ertl_to_ertlptr prog in
+∀stack_sizes.
+∀sigma : sigma_map trans_prog.
+∀st,st',f,fn,fl,called,args.
+ fetch_statement ERTL_semantics …
+  (globalenv_noinit ? prog) (pc … (sigma_state_pc ? sigma st)) =
+    return 〈f, fn,  final … (TAILCALL ERTL … fl called args)〉 → 
+ eval_state ERTL_semantics
+   (prog_var_names (joint_function ERTL_semantics) ℕ prog) 
+   (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes)) 
+   (sigma_state_pc ? sigma st) =
+  return st' →
+  ∃ st''. st' = sigma_state_pc ? sigma st'' ∧
+  ∃is_tailcall, is_tailcall'.
+  joint_tailcall_ident (mk_prog_params ERTLptr_semantics trans_prog stack_sizes) «st, is_tailcall'» =
+  joint_tailcall_ident (mk_prog_params ERTL_semantics prog stack_sizes) «(sigma_state_pc ? sigma st), is_tailcall» ∧
+  eval_state … (ev_genv … (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
+    st = return st''.
+cases daemon
+qed.
+
+lemma eval_cond_ok :
+∀prog.
+let trans_prog ≝ ertl_to_ertlptr prog in
+∀stack_sizes.
+∀sigma : sigma_map trans_prog.
+∀st,st',f,fn,a,ltrue,lfalse.
+ fetch_statement ERTL_semantics …
+  (globalenv_noinit ? prog) (pc … (sigma_state_pc ? sigma st)) =
+    return 〈f, fn,  sequential … (COND ERTL … a ltrue) lfalse〉 →
+ eval_state ERTL_semantics
+   (prog_var_names (joint_function ERTL_semantics) ℕ prog) 
+   (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes)) 
+   (sigma_state_pc ? sigma st) =
+  return st' → 
+as_costed (ERTL_status prog stack_sizes)
+  st' → 
+∃ st''. st' = sigma_state_pc ? sigma st'' ∧
+∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes)
+st st''.
+bool_to_Prop (taaf_non_empty … taf).
+cases daemon
+qed.
+ 
        
 inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
@@ -1883 +2350 @@
 (*interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).*)
 
-lemma linearise_ok:
+lemma
+  find_funct_ptr_none:
+    ∀A,B,V,iV. ∀p: program A V. ∀transf: (∀vs. A vs → B vs).
+    ∀b: block.
+    find_funct_ptr ? (globalenv … iV p) b = None ? →
+    find_funct_ptr ? (globalenv … iV (transform_program … p transf)) b = None ?.
+#A #B #V #i #p #transf #b 
+whd in match find_funct_ptr; normalize nodelta
+cases b -b * normalize nodelta [#x #_ %] * normalize nodelta 
+[1,2: [2: #x] #_ %] #x whd in match globalenv; normalize nodelta
+whd in match globalenv_allocmem; normalize nodelta
+cases daemon (*forse e' falso *)
+qed.
+
+lemma as_label_ok : ∀ prog : ertl_program.
+let trans_prog ≝ ertl_to_ertlptr prog in
+∀ sigma : sigma_map trans_prog.
+∀stack_sizes.
+∀ st.
+as_label (ERTLptr_status trans_prog stack_sizes) st = as_label 
+(ERTL_status prog stack_sizes) (sigma_state_pc prog sigma st).
+#prog #sigma #stack_size * #st #pc #lp
+whd in match as_label; normalize nodelta whd in match (as_pc_of ??) in ⊢ (??%%);
+whd in match (as_label_of_pc ??) in ⊢ (??%%); 
+
+
+(*
+
+whd in match fetch_statement; normalize nodelta
+whd in match sigma_state_pc; normalize nodelta @if_elim
+[ #EQbl whd in match fetch_internal_function; normalize nodelta >m_bind_bind
+ lapply(fetch_function_no_minus_one ??????) [2: @(pc_block pc) | lapply EQbl
+ @eqZb_elim #H * @H| @(ertl_to_ertlptr prog) |7: #EQ >EQ |*:] normalize nodelta
+ whd in match dummy_state_pc; whd in match (as_label_of_pc ??); whd in match null_pc;
+ whd in match fetch_statement; normalize nodelta whd in match fetch_internal_function;
+ normalize nodelta >m_bind_bind 
+ lapply(fetch_function_no_zero ??????) [2: @( «mk_block Code OZ,refl region Code»)
+ | % | @prog |7: #EQ >EQ |*:] %
+| inversion ( fetch_internal_function
+     (joint_closed_internal_function ERTL
+      (prog_var_names (joint_function ERTL) ℕ prog))
+     (globalenv_noinit (joint_function ERTL) prog) (pc_block pc))
+ [ * #id #fn #fn_spec #_ lapply(fetch_internal_function_transf ??????? fn_spec)
+   [ @(λvars,fn.translate_internal … fn) |] #EQ >EQ >m_return_bind normalize nodelta
+     whd in match (as_label_of_pc ??);
+     whd in match fetch_statement; normalize nodelta >fn_spec >m_return_bind
+     cases daemon (*serve specifica su sigma TODO*)
+   | #err #EQ lapply(jmeq_to_eq ??? EQ) -EQ #fetch_err #_ normalize nodelta 
+     whd in match dummy_state_pc; 
+     whd in match (as_label_of_pc ??); whd in match null_pc;
+     whd in match fetch_statement; normalize nodelta 
+     whd in match fetch_internal_function in ⊢ (???%);
+     normalize nodelta 
+     lapply(fetch_function_no_zero ??????) [2: @( «mk_block Code OZ,refl region Code»)
+     | % | @prog |7: #EQ >EQ in ⊢ (???%); |*:] normalize nodelta -EQ
+     lapply fetch_err -fetch_err whd in match fetch_internal_function; normalize nodelta
+     inversion(fetch_function ???) 
+     [* #id * #fn #fn_spec >m_return_bind normalize nodelta [whd in ⊢ (??%? → ?); #EQ destruct]
+     #EQ destruct  lapply(jmeq_to_eq ??? fn_spec) -fn_spec #fn_spec 
+     lapply(fetch_function_transf ????????? fn_spec) [ #v  @transf_fundef [2:@translate_internal |]|]
+     #EQ >EQ >m_return_bind %
+   | #err1 #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQfetch whd in ⊢ (??%? → ?); #EQ destruct 
+     normalize nodelta lapply EQfetch -EQfetch whd in match fetch_function;
+     normalize nodelta check joint_function
+      lapply(symbol_for_block_transf  ? ? ? ? prog (λvars.?)  (pc_block pc))
+      [@transf_fundef [2: @translate_internal|] |4: #EQ >EQ in ⊢ (? → %); |*:]  
+     cases(symbol_for_block ???) [ whd in ⊢ (??%% → ?); #EQ destruct %]
+     #id >m_return_bind inversion(find_funct_ptr ???)
+     [2: #fn1 #_ >m_return_bind whd in ⊢ (??%? → ?); #EQ destruct] 
+     #EQf whd in ⊢ (??%? → ?); #EQ destruct 
+     lapply(find_funct_ptr_none ??????? EQf) (*forse e' falso*)
+     [#vars @transf_fundef [2: @translate_internal|]|]
+     #EQ >EQ %
+     ]
+  ]
+]*)
+cases daemon
+qed.
+
+
+lemma ertl_to_ertlptr_ok:
  ∀prog.
   let trans_prog ≝ ertl_to_ertlptr prog in
@@ -1894 +2441 @@
 whd in match ERTL_status; whd in match ERTLptr_status; normalize nodelta
 whd in ⊢ (% → % → % → % → ?); #st1 #st1' #st2
-whd in match eval_state; normalize nodelta @('bind_inversion) ** #id #fn #stmt
-#H lapply (err_eq_from_io ????? H) -H #EQfetch @('bind_inversion) #st #EQst
-#EQst1' whd in match ERTLptrStatusSimulation; normalize nodelta
-#EQsim whd in match joint_abstract_status in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); 
-normalize nodelta whd in match joint_classify; normalize nodelta >EQfetch 
->m_return_bind cases stmt in EQst EQst1'; -stmt normalize nodelta
-[ * [#called #c_arg #c_dest | #reg #lbl | #seq ] #succ_pc | #fin_step | (*FCOND absurd*) cases daemon]
-[3: whd in match joint_classify_step; normalize nodelta whd in match eval_statement_no_pc;
-   normalize nodelta #H1 whd in match eval_statement_advance; normalize nodelta
-   whd in match set_no_pc; whd in match next; whd in match set_pc; normalize nodelta
-   #EQtobdest >EQsim in H1; #H1 cases(eval_seq_no_pc_no_call_ok ????????? H1) 
-     [2: cases daemon (*TODO*)] #st' * #st_spec' #st_sim % 
-         [% [ @st'| @(pc … st1') | @(last_pop … st1')]]
-         check taa_base 
-         %{(taaf_step ???? (taa_base … st2) ? ?)} 
-          [(*dalla commutazione del fetch TODO*) cases daemon
-          | whd in match (as_execute ???); whd in match eval_state; normalize nodelta
-           cases daemon (*dalla commutazione del fetch + st_spec' TODO *)
-          ] normalize nodelta % [% // cases daemon (*facile TODO *)] whd in match label_rel;
-           normalize nodelta (*specifica di sigma TODO *) cases daemon
-|       
-   
-
-
->EQsim in EQfetch; whd in match sigma_state_pc in ⊢ (%→ ?);
-whd in match fetch_statement; normalize nodelta #H @('bind_inversion H) -H
-* #id1 #fn1 whd in match fetch_internal_function; normalize nodelta 
-#H @('bind_inversion H) -H * #id2 #fn2 @if_elim #block_st2_spec
-[whd in match dummy_state_pc; whd in match null_pc; normalize nodelta
- lapply(fetch_function_no_zero ??????)
- [2: @(«mk_block Code OZ,refl region Code»)|%|@prog|7: #EQ >EQ |*:]
- whd in ⊢ (???% → ?); #ABS destruct]
- inversion(fetch_function
-          (fundef
-           (joint_closed_internal_function ERTLptr
-            (prog_var_names (joint_function ERTLptr) ℕ (ertl_to_ertlptr prog))))
-          (globalenv_noinit (joint_function ERTLptr) (ertl_to_ertlptr prog))
-          (pc_block (pc ERTLptr_semantics st2))) 
-[2: #err #_ normalize nodelta whd in match dummy_state_pc; whd in match null_pc; normalize nodelta
- lapply(fetch_function_no_zero ??????)
- [2: @(«mk_block Code OZ,refl region Code»)|%|@prog|7: #EQ >EQ |*:]
- whd in ⊢ (???% → ?); #ABS destruct] * #id3 #fn3 #EQ  lapply(jmeq_to_eq ??? EQ) -EQ
- #EQffst2 >m_return_bind cases fn3 in EQffst2; -fn3 [2: #ext #_ normalize nodelta
- whd in match dummy_state_pc; whd in match null_pc; normalize nodelta
- lapply(fetch_function_no_zero ??????)
- [2: @(«mk_block Code OZ,refl region Code»)|%|@prog|7: #EQ >EQ |*:]
- whd in ⊢ (???% → ?); #ABS destruct] #fn3 #fn3_spec normalize nodelta 
- #fn2_spec >(fetch_function_transf ??????????) in fn3_spec; [2: @fn2_spec|*:]
- cases fn2 in fn2_spec; -fn2 #fn2 #fn2_spec whd in match transf_fundef;
- normalize nodelta whd in ⊢ (??%? → ?); #EQ destruct whd in ⊢ (??%% → ?); #EQ destruct
- #H @('bind_inversion H) -H #stmt1 #H lapply(opt_eq_from_res ???? H) -H #stmt1_spec
- whd in ⊢ (??%% → ?); #EQ destruct cases stmt in stmt1_spec EQst1' EQst; -stmt
- [* [#called #c_arg #c_dest | #reg #lbl | #seq ] #succ_pc | #fin_step | (*FCOND absurd*) cases daemon]
- #stmt_spec whd in match eval_statement_advance; normalize nodelta whd in match eval_call;
- normalize nodelta #EQst1' whd in match eval_statement_no_pc; normalize nodelta 
-[3: #H cases(eval_seq_no_pc_no_call_ok ????????? H) [2: whd in match fetch_internal_function;
-    normalize nodelta whd in match sigma_state_pc; normalize nodelta @if_elim 
-    [ #H1 >H1 in block_st2_spec; *] #_ whd in match fetch_internal_function; normalize nodelta
-    >(fetch_function_transf ??????????) [2: @fn2_spec |*: ] whd in match transf_fundef;
-    normalize nodelta >fn2_spec >m_return_bind %] #st3 * #st3_spec #sem_rel
-    % [ % [ @st3 | @(pc … st1') | @(last_pop … st2)]] % [%2 [2: %1|1:|4: whd in match as_classifier; normalize nodelta whd in match (as_classify ??); normalize nodelta
-    
-    %{(taaf_step … (taa_base …) …) I}
- 
- 
- [1,2,4: whd in ⊢ (??%% → ?); #EQ destruct 
- |3: whd in EQst1' : (??%%); whd in match set_no_pc in EQst1'; normalize nodelta in EQst1';
-    whd in match sigma_state_pc in EQst1'; normalize nodelta in EQst1';
-    >block_st2_spec in EQst1'; @if_elim [ #H >H in block_st2_spec; *] #_ 
-    whd in match fetch_internal_function; normalize nodelta >(fetch_function_transf ??????????) [2: @fn2_spec|*:]
-    >m_return_bind whd in match transf_fundef; normalize nodelta whd in match next;
-    normalize nodelta whd in match set_pc; normalize nodelta #EQ destruct #H
-
-    
-
-    
-    whd ;in match  in EQst1';
-    destruct #EQst
- #EQst normalize nodelta
- [ whd in match joint_classify_step; normalize nodelta
- 
- 
- 
- lapply(fetch_function_no_zero ??????) [2: @(«mk_block Code OZ,refl region Code») 
- |2: % | %|7: #EQ >EQ *: try assumption
-
- normalize in ⊢ (%→ ?);
-normalize in as_ex;
-
-
-
+change with
+  (eval_state ERTL_semantics (prog_var_names ???) ?? = ? → ?)
+#EQeval @('bind_inversion EQeval)
+** #id #fn #stmt #H lapply (err_eq_from_io ????? H) -H #EQfetch
+#_  whd in match ERTLptrStatusSimulation; normalize nodelta #EQst2 destruct
+cases stmt in EQfetch; -stmt
+[ * [#called #c_arg #c_dest | #reg #lbl | #seq ] #succ_pc | #fin_step | *]
+normalize nodelta #EQfetch
+change with (joint_classify ??) in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
+[ (*CALL*)
+  cases daemon (*TODO*) 
+| whd in match joint_classify; normalize nodelta
+ >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
+  normalize nodelta
+ #n_cost 
+ cases (eval_cond_ok … EQfetch EQeval n_cost)
+ #st3 * #EQ destruct * #taf #tafne %{st3} %{taf} 
+ % [ % [2: %] >tafne normalize nodelta @I] whd >as_label_ok %
+| whd in match joint_classify; normalize nodelta
+ >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
+  normalize nodelta
+  cases (eval_seq_no_call_ok ?????????  EQfetch EQeval)
+  #st3 * #EQ destruct *  #taf #tafne %{st3} %{taf} >tafne normalize nodelta
+  % [% //] whd >as_label_ok [2:assumption] %
+| (*FIN*) 
+  cases fin_step in EQfetch;
+  [ (*GOTO*) #lbl #EQfetch  whd in match joint_classify; normalize nodelta
+  >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
+    cases (eval_goto_ok … EQfetch EQeval)
+    #st3 * #EQ destruct * #taf #tarne %{st3} %{taf} >tarne normalize nodelta
+    % [% //] whd >as_label_ok [2:assumption] %
+  | (*RETURN*) #EQfetch
+     whd in match joint_classify; normalize nodelta
+    >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
+    cases (eval_return_ok … EQfetch EQeval) #is_ret
+    * #st3 * #EQ destruct * #after_ret * #taf ** #taf_prf #EQeval' #ret_prf
+    % [2: % [2: % [2: %{(taa_base …)} %{taf}] |*: ] |*:]
+    % [2: whd >as_label_ok %] % [2: assumption] % [2: %] % [2: assumption]
+    % assumption
+  | (*TAILCALL*) #fl #called #args #EQfetch 
+    cases (eval_tailcall_ok … EQfetch EQeval) #st3 * #EQ destruct * #is_tailcall 
+    * #is_tailcall' *  #eq_call #EQeval' >is_tailcall normalize nodelta
+    #prf  %{«?, is_tailcall'»} %{eq_call}
+    % [2: % [2: %{(taa_base …)} %{(taa_base …)}  % [ %{EQeval'} % |] | ] | ]
+    whd >as_label_ok %
+  ]
+]
+qed.
+
+
+

src/joint/semantics.ma

@@ -77 +77 @@
   mk_program_counter «mk_block Code (-1), refl …» one.
 
-definition null_pc : program_counter ≝ 
-    mk_program_counter «mk_block Code OZ, refl …» one.
+definition null_pc : Pos →  program_counter ≝ λpos.
+    mk_program_counter «mk_block Code OZ, refl …» pos.
 
 definition set_m: ∀p. bemem → state p → state p ≝