Changeset 1882 for src/joint

Timestamp:

Apr 6, 2012, 8:02:10 PM (8 years ago)

Author:

tranquil

Message:

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

Location:

src/joint

Files:

• BEMem.ma (modified) (4 diffs)
• Joint_paolo.ma (modified) (11 diffs)
• TranslateUtils_paolo.ma (modified) (9 diffs)
• blocks.ma (added)
• semanticsUtils_paolo.ma (modified) (7 diffs)
• semantics_blocks.ma (added)
• semantics_paolo.ma (modified) (20 diffs)

src/joint/BEMem.ma

@@ -44 +44 @@
      mk_mem … blocks (nextblock … m) (nextblock_pos … m)).
 
+definition is_addressable : region → bool ≝ λr.match r with
+  [ XData ⇒ true | Code ⇒ true | _ ⇒ false ].
+
+
+definition is_address : (beval × beval) → Prop ≝ λa.
+  ∃p : Σp.bool_to_Prop (is_addressable (ptype p)).∃p0,p1.
+    \fst a = BVptr p p0 ∧ part_no ? p0 = 0 ∧
+    \snd a = BVptr p p1 ∧ part_no ? p1 = 1.
+
+definition is_addressb : (beval × beval) → bool ≝ λa.
+  match a with
+  [ mk_Prod a0 a1 ⇒
+    match a0 with
+    [ BVptr p0 part0 ⇒
+      is_addressable (ptype p0) ∧ eqb part0 0 ∧
+        match a1 with
+        [ BVptr p1 part1 ⇒
+          eq_pointer p0 p1 ∧ eqb part1 1
+        | _ ⇒ false
+        ]
+    | _ ⇒ false
+    ]
+  ].
+
+lemma is_addressb_elim : ∀P : bool → Prop.∀a : beval × beval.
+  (is_address a → P true) → (¬is_address a → P false) → P (is_addressb a).
+#P * *
+[4:|*: [|#b0|#r0#part0] #a1 #_ #Pfalse @Pfalse % * #x * #p0 * #p1 *** #EQ destruct(EQ)]
+#p0 #part0 #a1
+whd in match is_addressb; normalize nodelta
+elim (true_or_false_Prop (is_addressable (ptype p0)))
+#H >H
+[ @(eqb_elim part0 0) #Heq
+  [ cases a1 [|#b0|#r0#part0|#p1#part1] whd in match (?∧?);
+    [4: @eq_pointer_elim #Heq'
+      [ @(eqb_elim part1 1) #Heq''
+        [ #Ptrue #_ @Ptrue destruct
+          %{p1} [assumption] %{part0} %{part1}
+          % [ % [ % ]] try % assumption
+        ]
+      ]
+    ]
+  ]
+]
+#_ #Pfalse @Pfalse % ** #p0' #H' * #part0' * #part1' ***
+#H0 #H1 #H2 #H3 destruct /2 by absurd/
+qed.
+
 (* CSC: only pointers to XRAM or code memory ATM *)
 definition address ≝ beval × beval.
+definition safe_address ≝ Sig address is_address.
+unification hint 0 ≔ ;
+P ≟ Prod beval beval
+(*------------------*)⊢
+safe_address ≡ Sig P is_address.
 
 definition eq_address: address → address → bool ≝
@@ -53 +106 @@
 definition pointer_of_address: address → res pointer ≝
  λp. let 〈v1,v2〉 ≝ p in pointer_of_bevals [v1;v2].
-definition address_of_pointer: pointer → res address ≝ beval_pair_of_pointer.
-
-definition code_pointer_of_address: address → res (Σp:pointer. ptype p = Code) ≝ code_pointer_of_beval_pair.
+ 
+definition pointer_of_address_safe : safe_address → pointer ≝
+  λp.match \fst p return λx.\fst p = x → ? with
+    [ BVptr ptr _ ⇒ λ_.ptr
+    | _ ⇒ λabs.⊥
+    ] (refl …).
+lapply abs -abs cases p
+* #a0 #a1 * #x * #p0 * #p1 *** #H0 #H1 #H2 #H3 #H4
+destruct(H0 H4)
+qed.
+
+definition pointer_compat' ≝ λb,r.
+  match b with
+  [ mk_block r' z ⇒
+    if eq_region r' r then True
+    else
+      match r with
+      [ Any ⇒ True
+      | XData ⇒ match r' with
+        [ PData ⇒ True
+        | _ ⇒ False
+        ]
+      | _ ⇒ False
+      ]
+   ].
+
+lemma pointer_compat_to_ind : ∀b,r.pointer_compat' b r → pointer_compat b r.
+** #z ** //
+qed.
+
+lemma pointer_compat_from_ind : ∀b,r.pointer_compat b r → pointer_compat' b r.
+#b #r #H inversion H
+[ #s #id #EQ1 #EQ2 #EQ3 whd >reflexive_eq_region %
+| #id #EQ1 #EQ2 #EQ3 %
+| #r #id #EQ1 #EQ2 #EQ3 whd @eq_region_elim #EQ4 destruct(EQ4) %
+]
+qed.
+
+lemma pointer_of_address_is_safe : ∀a : safe_address.pointer_of_address a = OK … (pointer_of_address_safe a).
+** #a0 #a1 ***** #r #z #Hr #o * lapply (pointer_compat_from_ind ?? Hr)
+cases r in Hr ⊢ %; #Hr *
+** #part0 #H0 ** #part1 #H1 *** #EQa0 #EQpart0 #EQa1 #EQpart1
+destruct normalize
+@eqZb_elim [2,4,6: * #ABS elim (ABS (refl …))]
+@eqZb_elim [2,4,6: * #ABS elim (ABS (refl …))]
+#_ #_ normalize %
+qed.
+    
+definition address_of_pointer : pointer → res address ≝ beval_pair_of_pointer.
+
+example address_of_pointer_OK_to_safe :
+  ∀p,a.address_of_pointer p = OK … a → is_address a.
+#p
+lapply (refl … p)
+generalize in match p in ⊢ (???%→%); **
+whd in match (address_of_pointer ?);
+#b #H #o #EQp * #a0 #a1
+normalize #EQ destruct(EQ)
+%{p} >EQp [1,3: %]
+% [2,4: % [2,4: % [1,3: % [1,3: %]]]] %
+qed.
+
+definition safe_address_of_pointer: pointer → res safe_address ≝ λp.
+  do a as EQ ← address_of_pointer p ; return «a ,address_of_pointer_OK_to_safe ?? EQ».
+
+lemma address_of_pointer_is_safe :
+  ∀p.address_of_pointer p = ! a ← safe_address_of_pointer p ; return (a : address).
+****#z #H
+lapply (pointer_compat_from_ind ?? H) * #o
+normalize %
+qed.
+
+definition code_pointer_of_address: address → res (Σp:pointer. ptype p = Code) ≝
+code_pointer_of_beval_pair.
+
 definition address_of_code_pointer: (Σp:pointer. ptype p = Code) → address ≝ beval_pair_of_code_pointer.
 
+definition safe_address_of_code_pointer: (Σp:pointer. ptype p = Code) → safe_address ≝ address_of_code_pointer.
+cases H -H * #r #b #H #o #EQ destruct(EQ) normalize lapply H
+lapply (pointer_compat_from_ind … H) -H cases b * #z * #H
+%{«mk_pointer ? (mk_block Code z) H o,I»}
+% [2: % [2: % [ % [ % ]] % |]|]
+qed.
+
+(* Paolo: why only code pointers and not XRAM too? *)
 definition addr_add: address → nat → res address ≝
  λaddr,n.
@@ -65 +198 @@
 qed.
 
+definition safe_addr_add: safe_address → nat → res safe_address ≝
+ λaddr,n.
+  do ptr ← code_pointer_of_address addr ;
+  OK … (safe_address_of_code_pointer (shift_pointer 16 ptr (bitvector_of_nat … n))).
+normalize cases ptr #p #E @E
+qed.
+
 definition addr_sub: address → nat → res address ≝
  λaddr,n.
@@ -71 +211 @@
 normalize cases ptr #p #E @E
 qed.
+
+definition safe_addr_sub: safe_address → nat → res safe_address ≝
+ λaddr,n.
+  do ptr ← code_pointer_of_address addr ;
+  OK … (safe_address_of_code_pointer (neg_shift_pointer 16 ptr (bitvector_of_nat … n))).
+normalize cases ptr #p #E @E
+qed.

src/joint/Joint_paolo.ma

@@ -4 +4 @@
 include "common/Registers.ma".
 include "common/Graphs.ma".
+include "utilities/lists.ma".
+include "common/LabelledObjects.ma".
+include "ASM/Util.ma".
 
 (* Here is the structure of parameter records (downward edges are coercions,
@@ -12 +15 @@
 
         lin_params      graph_params
-          |       \_____ /____   |
-          |             /     \  |
-          \_______     /      ↓  ↓
-                  \   _\____ params
-                   \_/  \      |
-                    / \  \     ↓
-              _____/   unserialized_params
-             /      _______/   | 
-            /      /           | 
-     stmt_params  /   local_params
-        |      __/             |
-    inst_params       funct_params
-
-inst_params : types needed to define instructions
+              |   \_____ /____   |
+              |         /     \  |
+              |        /      ↓  ↓
+              |       |      params
+              |       |        |
+              |       |   stmt_params
+              |       |    /    
+          unserialized_params             
+            |            \       
+            |             \      
+            |         local_params
+            |              |    
+    step_params       funct_params
+
+step_params : types needed to define steps (stmts with a default fallthrough)
 stmt_params : adds successor type needed to define statements
 funct_params : types of result register and parameters of function
 local_params : adds types of local registers
-params : adds type of code and lookup function
-graph_params : is made just of inst_params and local_params, and the coercion
-  to params adds structure common to graph languages *)
-
-record inst_params : Type[1] ≝ 
+params : adds type of code and related properties *)
+
+record step_params : Type[1] ≝ 
  { acc_a_reg: Type[0] (* registers that will eventually need to be A *)
  ; acc_b_reg: Type[0] (* registers that will eventually need to be B *)
@@ -46 +48 @@
  ; call_args: Type[0] (* arguments of function calls *)
  ; call_dest: Type[0] (* possible destination of function computation *)
- ; ext_instruction: Type[0] (* other instructions not fitting in the general framework *)
- ; ext_forall_labels : (label → Prop) → ext_instruction → Prop
- ; ext_fin_instruction: Type[0] (* final instructions (e.g. tailcalls) not fitting in the general framework *)
- ; ext_fin_forall_labels : (label → Prop) → ext_fin_instruction → Prop
+ ; ext_step: Type[0] (* other instructions not fitting in the general framework *)
+ ; ext_step_labels : ext_step → list label
+ ; ext_fin_stmt: Type[0] (* final instructions (e.g. tailcalls) not fitting in the general framework *)
+ ; ext_fin_stmt_labels : ext_fin_stmt → list label
  }.
  
-inductive joint_instruction (p:inst_params) (globals: list ident): Type[0] ≝
-  | COMMENT: String → joint_instruction p globals
-  | COST_LABEL: costlabel → joint_instruction p globals
-  | MOVE: pair_move p → joint_instruction p globals
-  | POP: acc_a_reg p → joint_instruction p globals
-  | PUSH: acc_a_arg p → joint_instruction p globals
-  | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_instruction p globals
-  | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_instruction p globals
-  | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_instruction p globals
-  | OP2: Op2 → acc_a_reg p → acc_a_arg p → snd_arg p → joint_instruction p globals
+inductive joint_step (p:step_params) (globals: list ident): Type[0] ≝
+  | COMMENT: String → joint_step p globals
+  | COST_LABEL: costlabel → joint_step p globals
+  | MOVE: pair_move p → joint_step p globals
+  | POP: acc_a_reg p → joint_step p globals
+  | PUSH: acc_a_arg p → joint_step p globals
+  | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_step p globals
+  | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_step p globals
+  | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_step p globals
+  | OP2: Op2 → acc_a_reg p → acc_a_arg p → snd_arg p → joint_step p globals
   (* int done with generic move *)
-(*| INT: generic_reg p → Byte → joint_instruction p globals *)
-  | CLEAR_CARRY: joint_instruction p globals
-  | SET_CARRY: joint_instruction p globals
-  | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_instruction p globals
-  | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_instruction p globals
-  | CALL_ID: ident → call_args p → call_dest p → joint_instruction p globals
-  | COND: acc_a_reg p → label → joint_instruction p globals
-  | extension: ext_instruction p → joint_instruction p globals.
-
-coercion extension_to_instruction :
-  ∀p,globals.∀c : ext_instruction p.joint_instruction p globals ≝
-  extension
-  on _c : ext_instruction ? to joint_instruction ??.
-
-notation "r ← a1 .op. a2" with precedence 50 for
+(*| INT: generic_reg p → Byte → joint_step p globals *)
+  | CLEAR_CARRY: joint_step p globals
+  | SET_CARRY: joint_step p globals
+  | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_step p globals
+  | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_step p globals
+  | CALL_ID: ident → call_args p → call_dest p → joint_step p globals
+  | COND: acc_a_reg p → label → joint_step p globals
+  | extension: ext_step p → joint_step p globals.
+
+notation "r ← a1 .op. a2" with precedence 55 for
   @{'op2 $op $r $a1 $a2}.
-notation "r ← . op . a" with precedence 50 for
+notation "r ← . op . a" with precedence 55 for
   @{'op1 $op $r $a}.
-notation "r ← a" with precedence 50 for
+notation "r ← a" with precedence 55 for
   @{'mov $r $a}. (* to be set in individual languages *)
 notation "❮r, s❯ ← a1 . op . a2" with precedence 50 for
@@ -90 +87 @@
 interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2).
 
-
-definition inst_forall_labels : ∀p : inst_params.∀globals.
-    (label → Prop) → joint_instruction p globals → Prop ≝
-λp,g,P,inst. match inst with
-  [ COND _ l ⇒ P l
-  | extension ext_s ⇒ ext_forall_labels p P ext_s
-  | _ ⇒ True
- ].
-
+coercion extension_to_step : ∀p,globals.∀s : ext_step p.joint_step p globals ≝
+  extension on _s : ext_step ? to joint_step ??.
+
+definition step_labels ≝
+  λp, globals.λs : joint_step p globals.
+    match s with
+    [ COND _ l ⇒ [l]
+    | extension ext_s ⇒ ext_step_labels ? ext_s
+    | _ ⇒ [ ]
+    ].
+
+definition step_forall_labels : ∀p : step_params.∀globals.
+    (label → Prop) → joint_step p globals → Prop ≝
+λp,g,P,inst. All … P (step_labels … inst).
+ 
 record funct_params : Type[1] ≝
   { resultT : Type[0]
@@ -109 +112 @@
  }.
 
+
 record unserialized_params : Type[1] ≝
- { u_inst_pars :> inst_params
+ { u_inst_pars :> step_params
  ; u_local_pars :> local_params
  }.
 
 record stmt_params : Type[1] ≝
-  { unserialized_pars :> unserialized_params
+  { uns_pars :> unserialized_params
   ; succ : Type[0]
-  ; succ_forall_labels : (label → Prop) → succ → Prop
+  ; succ_label : succ → option label
   }. 
 
 inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝
-  | sequential: joint_instruction p globals → succ p → joint_statement p globals
+  | sequential: joint_step p globals → succ p → joint_statement p globals
   | GOTO: label → joint_statement p globals
   | RETURN: joint_statement p globals
-  | extension_fin : ext_fin_instruction p → joint_statement p globals.
-
-coercion extension_fin_to_statement :
-  ∀p : stmt_params.∀globals.∀c : ext_fin_instruction p.joint_statement p globals ≝
-  extension_fin
-  on _c : ext_fin_instruction ? to joint_statement ??.
+  | extension_fin : ext_fin_stmt p → joint_statement p globals.
+
+coercion extension_fin_to_stmt : ∀p : stmt_params.∀globals.∀s : ext_fin_stmt p.joint_statement p globals ≝
+  extension_fin on _s : ext_fin_stmt ? to joint_statement ??.
+
+definition no_seq ≝ λp : stmt_params.λglobals.λs : joint_statement p globals.
+  match s with
+  [ sequential _ _ ⇒ False
+  | _ ⇒ True
+  ].
 
 record params : Type[1] ≝
  { stmt_pars :> stmt_params
  ; codeT: list ident → Type[0]
- ; code_has_label: ∀globals.codeT globals → label → Prop
- ; forall_statements : ∀globals.(joint_statement stmt_pars globals → Prop) →
-    codeT globals → Prop
+ ; code_point : Type[0]
+ ; stmt_at : ∀globals.codeT globals → code_point → option (joint_statement stmt_pars globals)
+ ; point_of_label : ∀globals.codeT globals → label → option code_point
+ ; point_of_succ : code_point → succ stmt_pars → code_point
  }.
 
-
-definition stmt_forall_labels : ∀p : stmt_params.∀globals.
-    (label → Prop) → joint_statement p globals → Prop ≝
-  λp,g,P,stmt. match stmt with
-  [ sequential inst next ⇒ inst_forall_labels p g P inst ∧ succ_forall_labels p P next
-  | GOTO l ⇒ P l
-  | RETURN ⇒ True
-  | extension_fin c ⇒ ext_fin_forall_labels … P c
+definition code_has_point ≝
+  λp,globals,c,pt.match stmt_at p globals c pt with [Some _ ⇒ true | None ⇒ false].
+
+interpretation "code membership" 'mem p c = (code_has_point ?? c p).
+
+definition point_in_code ≝ λp,globals,code.Σpt.bool_to_Prop (code_has_point p globals code pt).
+unification hint 0 ≔ p, globals, code ⊢ point_in_code p globals code ≡ Sig (code_point p) (λpt.bool_to_Prop (code_has_point p globals code pt)).
+
+definition stmt_at_safe ≝ λp,globals,code.λpt : point_in_code p globals code.
+  match pt with
+  [ mk_Sig pt' pt_prf ⇒
+    match stmt_at … code pt' return λx.stmt_at … code pt' = x → ? with
+    [ Some x ⇒ λ_.x
+    | None ⇒ λabs.⊥
+    ] (refl …)
+  ]. normalize in pt_prf;
+    >abs in pt_prf; // qed.
+
+definition forall_statements : ∀p : params.∀globals.pred_transformer (joint_statement p globals) (codeT p globals)  ≝
+  λp,globals,P,c. ∀pt,s.stmt_at ?? c pt = Some ? s → P s.
+
+definition forall_statements_i :
+  ∀p : params.∀globals.(code_point p → joint_statement p globals → Prop) →
+    codeT p globals → Prop  ≝
+  λp,globals,P,c. ∀pt,s.stmt_at ?? c pt = Some ? s → P pt s.
+
+lemma forall_statements_mp : ∀p,globals.modus_ponens ?? (forall_statements p globals).
+#p #globals #P #Q #H #y #G #pnt #s #EQ @H @(G … EQ) qed.
+
+lemma forall_statements_i_mp : ∀p,globals.∀P,Q.(∀pt,s.P pt s → Q pt s) →
+  ∀c.forall_statements_i p globals P c → forall_statements_i p globals Q c.
+#p #globals #P #Q #H #y #G #pnt #s #EQ @H @(G … EQ) qed.
+
+definition code_has_label ≝ λp,globals,c,l.
+  match point_of_label p globals c l with
+  [ Some pt ⇒ code_has_point … c pt
+  | None ⇒ false
   ].
+
+definition stmt_explicit_labels :
+  ∀p,globals.
+  joint_statement p globals → list label ≝
+  λp,globals,stmt. match stmt with
+  [ sequential c _ ⇒ step_labels … c
+  | GOTO l ⇒ [ l ]
+  | RETURN ⇒ [ ]
+  | extension_fin c ⇒ ext_fin_stmt_labels … c
+  ].
+
+definition stmt_implicit_label : ∀p,globals.joint_statement p globals →
+  option label ≝
+ λp,globals,s.match s with [ sequential _ s ⇒ succ_label … s | _ ⇒ None ?].
+  
+definition stmt_labels : ∀p : stmt_params.∀globals.
+    joint_statement p globals → list label ≝
+  λp,g,stmt.
+  (match stmt_implicit_label … stmt with
+     [ Some l ⇒ [l]
+     | None ⇒ [ ]
+     ]) @ stmt_explicit_labels … stmt.
+
+definition stmt_forall_labels ≝
+  λp, globals.λ P : label → Prop.λs : joint_statement p globals.
+  All … P (stmt_labels … s).
+
+lemma stmt_forall_labels_explicit : ∀p,globals,P.∀s : joint_statement p globals.
+  stmt_forall_labels … P s → All … P (stmt_explicit_labels … s).
+#p#globals#P #s
+whd in ⊢ (% → ?);
+whd in ⊢ (???% → ?);
+elim (stmt_implicit_label ???) [2: #next * #_] //
+qed.
+
+lemma stmt_forall_labels_implicit : ∀p,globals,P.∀s : joint_statement p globals.
+  stmt_forall_labels … P s →
+    opt_All … P (stmt_implicit_label … s).
+#p#globals#P#s
+whd in ⊢ (% → ?);
+whd in ⊢ (???% → ?);
+elim (stmt_implicit_label ???)
+[ //
+| #next * #Pnext #_ @Pnext
+]
+qed.
+
+definition code_forall_labels ≝
+  λp,globals,P,c.forall_statements p globals (stmt_forall_labels … P) c.
+
+lemma code_forall_labels_mp : ∀p,globals,P,Q.(∀l.P l → Q l) →
+  ∀c.code_forall_labels p globals P c → code_forall_labels … Q c ≝
+  λp,globals,P,Q,H.forall_statements_mp … (λs. All_mp … H ?).
 
 record lin_params : Type[1] ≝
   { l_u_pars :> unserialized_params }.
-
-include "utilities/option.ma".
+  
+lemma index_of_label_length : ∀tag,A,lbl,l.occurs_exactly_once ?? lbl l → lt (index_of_label tag A lbl l) (|l|).
+#tag #A #lbl #l elim l [*]
+** [2: #id] #a #tl #IH
+[ change with (if (eq_identifier ???) then ? else ?) in match (occurs_exactly_once ????);
+  change with (if (eq_identifier ???) then ? else ?) in match (index_of_label ????);
+  @eq_identifier_elim #Heq normalize nodelta
+  [ #_ normalize / by /]
+| whd in ⊢ (?%→?%?);
+]
+#H >(index_of_label_from_internal … H)
+@le_S_S @(IH H)
+qed.
+
+(* mv *)
+lemma nth_opt_hit_length : ∀A,l,n,x.nth_opt A n l = Some ? x → n < |l|.
+#A #l elim l normalize [ #n #x #ABS destruct(ABS)]
+#hd #tl #IH * [2:#n] #x normalize [#H @le_S_S @(IH … H)] /2 by /
+qed.
+
+lemma nth_opt_miss_length : ∀A,l,n.nth_opt A n l = None ? → n ≥ |l|.
+#A #l elim l [//] #hd #tl #IH * normalize [#ABS destruct(ABS)]
+#n' #H @le_S_S @(IH … H)
+qed.
+
+lemma nth_opt_safe : ∀A,l,n,prf.nth_opt A n l = Some ? (nth_safe A n l prf).
+#A #l elim l
+[ #n #ABS @⊥ /2 by absurd/
+| #hd #tl #IH * normalize //
+]
+qed.
 
 definition lin_params_to_params ≝
   λlp : lin_params.
      mk_params
-      (mk_stmt_params lp unit (λ_.λ_.True))
+      (mk_stmt_params lp unit (λ_.None ?))
     (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement ? globals)))
-    (* code_has_label ≝ *)(λglobals,code,lbl.Exists ?
-        (λl_stmt. \fst l_stmt = Some ? lbl) code)
-    (* forall_statements ≝ *)(λglobals,P,code.All ?
-        (λl_stmt. P (\snd l_stmt)) code).
+    (* code_point ≝ *)ℕ
+    (* stmt_at ≝ *)(λglobals,code,point.! ls ← nth_opt ? point code ; return \snd ls)
+    (* point_of_label ≝ *)(λglobals,c,lbl.
+      If occurs_exactly_once ?? lbl c then with prf do
+        return index_of_label ?? lbl c
+      else
+        None ?)
+    (* point_of_succ ≝ *)(λcurrent.λ_.S (current)).
 
 coercion lp_to_p : ∀lp : lin_params.params ≝ lin_params_to_params
   on _lp : lin_params to params.
+  
+lemma lin_code_has_point : ∀lp : lin_params.∀globals.∀code:codeT lp globals.
+  ∀pt.pt ∈ code = leb (S pt) (|code|).
+#lp #globals #code elim code
+[ #pt %
+| #hd #tl #IH * [%]
+  #n @IH
+]qed.
+
+lemma lin_code_has_label : ∀lp : lin_params.∀globals.∀code:codeT lp globals.
+  ∀lbl.code_has_label … code lbl = occurs_exactly_once ?? lbl code.
+#lp #globals #code #lbl
+whd in match (code_has_label ????);
+whd in match (point_of_label ????);
+elim (true_or_false_Prop (occurs_exactly_once ?? lbl code))
+#Heq >Heq normalize nodelta
+[ >lin_code_has_point @(leb_elim (S ?)) [#_ |
+  #ABS elim(absurd ?? ABS) -ABS
+  @index_of_label_length assumption ]] %
+qed.
 
 record graph_params : Type[1] ≝
   { g_u_pars :> unserialized_params }.
+
+(* move *)
+definition lookup_safe : ∀tag,A.∀m : identifier_map tag A.∀i.i ∈ m → A ≝
+  λtag,A,m.match m return λx : identifier_map tag A.∀i.i ∈ x → ? with
+  [ an_id_map m' ⇒ λi.match i return λx.x ∈ an_id_map ?? m' → ? with
+    [ an_identifier i' ⇒
+      match lookup_opt … i' m' return λx.match x with [Some y ⇒ true | None ⇒ false] → ? with
+      [ Some y ⇒ λ_.y
+      | None ⇒ Ⓧ
+      ]
+    ]
+  ].
+  
+lemma lookup_safe_elim : ∀tag,A.∀P : A → Prop.∀m,i,prf.
+  (∀x.lookup tag A m i = Some ? x → P x) → P (lookup_safe tag A m i prf).
+#tag #A #P *#m *#i normalize elim (lookup_opt A i m) normalize
+[ * ]
+#s * #H @H %
+qed.
 
 (* One common instantiation of params via Graphs of joint_statements
@@ -175 +338 @@
   λgp : graph_params.
      mk_params
-      (mk_stmt_params gp label (λP.P))
+      (mk_stmt_params gp label (Some ?))
     (* codeT ≝ *)(λglobals.graph (joint_statement ? globals))
-    (* code_has_label ≝ *)(λglobals,code,lbl.lookup … code lbl ≠ None ?)
-    (* forall_statements ≝ *)(λglobals,P,code.
-      ∀l,s.lookup … code l = Some ? s → P s).
-    
+    (* code_point ≝ *)label
+    (* stmt_at ≝ *)(λglobals,code.lookup LabelTag ? code)
+    (* point_of_label ≝ *)(λ_.λ_.λlbl.return lbl)
+    (* point_of_succ ≝ *)(λ_.λlbl.lbl).
+
 coercion gp_to_p : ∀gp:graph_params.params ≝ graph_params_to_params
 on _gp : graph_params to params.
-   
-
-definition labels_present : ∀globals.∀p : params.
-  codeT p globals → (joint_statement p globals) → Prop ≝
-λglobals,p,code,s. stmt_forall_labels p globals
-  (λl.code_has_label ?? code l) s.
+
+lemma graph_code_has_point : ∀gp : graph_params.∀globals.∀code:codeT gp globals.
+  ∀pt.code_has_point … code pt = mem_set … code pt.
+#gp#globals*#m*#i % qed.
+
+lemma graph_code_has_label : ∀gp : graph_params.∀globals.∀code:codeT gp globals.
+  ∀lbl.code_has_label … code lbl = mem_set … code lbl.
+#gp #globals * #m * #i % qed.
+
+definition stmt_forall_succ ≝ λp,globals.λP : succ p → Prop.
+  λs : joint_statement p globals.
+  match s with
+  [ sequential _ n ⇒ P n
+  | _ ⇒ True
+  ].
+
+definition statement_closed : ∀globals.∀p : params.
+  codeT p globals → code_point p → (joint_statement p globals) → Prop ≝
+λglobals,p,code,pt,s.
+  All ? (λl.bool_to_Prop (code_has_label ?? code l)) (stmt_explicit_labels … s) ∧
+  stmt_forall_succ … (λn.bool_to_Prop (point_of_succ ? pt n ∈ code)) s.
 
 definition code_closed : ∀p : params.∀globals.
   codeT p globals → Prop ≝ λp,globals,code.
-    forall_statements … (labels_present … code) code.
+    forall_statements_i … (statement_closed … code) code.
 
 (* CSC: special case where localsT is a list of registers (RTL and ERTL) *)
 definition rtl_ertl_params : ?→?→params ≝ λinst_pars,funct_pars.
-  (mk_graph_params (mk_unserialized_params inst_pars (mk_local_params funct_pars (list register)))).
+  (mk_graph_params (mk_unserialized_params inst_pars (mk_local_params funct_pars register))).
 
 record joint_internal_function (globals: list ident) (p:params) : Type[0] ≝
@@ -206 +385 @@
   joint_if_result   : resultT p;
   joint_if_params   : paramsT p;
-  joint_if_locals   : localsT p;
+  joint_if_locals   : list (localsT p); (* use void where no locals are present *)
 (*CSC: XXXXX stacksize unused for LTL-...*)
   joint_if_stacksize: nat;
   joint_if_code     : codeT p globals ;
-(*CSC: XXXXX entry unused for LIN, but invariant in that case... *)
-  joint_if_entry    : Σl: label. code_has_label … joint_if_code l;
-(*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *)
-  joint_if_exit     : Σl: label. code_has_label …  … joint_if_code l
+  joint_if_entry : point_in_code … joint_if_code ;
+  joint_if_exit : point_in_code … joint_if_code 
 }.
 
@@ -219 +396 @@
   λglobals,p.
     Σdef : joint_internal_function globals p. code_closed … (joint_if_code … def).
-
-(* Currified form *)
-definition set_joint_if_exit ≝
-  λglobals,pars.
-  λexit: label.
-  λp:joint_internal_function globals pars.
-  λprf: code_has_label … (joint_if_code … p) exit.
-   mk_joint_internal_function globals pars
-    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
-    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
-    (joint_if_code … p) (joint_if_entry … p) (mk_Sig … exit prf).
 
 definition set_joint_code ≝
@@ -244 +410 @@
 
 definition set_joint_if_graph ≝
-  λglobals,pars.
+  λglobals.λpars : graph_params.
   λgraph.
   λp:joint_internal_function globals pars.
-  λentry_prf: code_has_label … graph (joint_if_entry … p).
-  λexit_prf: code_has_label … graph (joint_if_exit … p).
+  λentry_prf.
+  λexit_prf.
     set_joint_code globals pars p 
       graph
-      (mk_Sig … (joint_if_entry … p) entry_prf)
-      (mk_Sig … (joint_if_exit … p) exit_prf).
+      (mk_Sig ?? (joint_if_entry ?? p) entry_prf)
+      (mk_Sig … (joint_if_exit ?? p) exit_prf).
 
 definition set_luniverse ≝
@@ -272 +438 @@
     (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
     
-(* Paolo: probably should move these elsewhere *)
-definition graph_dom ≝ λX.λg : graph X.Σl : label.lookup … g l ≠ None ?.
-definition graph_dom_add_incl : ∀X.∀g : graph X.∀l : label.∀x : X.
-  graph_dom ? g → graph_dom ? (add … g l x) ≝ λX,g,l,x,sig_l.
-  mk_Sig … (pi1 ?? sig_l) ?.
-@graph_add_lookup
-@(pi2 … sig_l)
-qed.
-
 (* Specialized for graph_params *)
 definition add_graph ≝
@@ -290 +447 @@
      (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
      code
-     (graph_dom_add_incl … (joint_if_entry … p))
-     (graph_dom_add_incl … (joint_if_exit … p)).
+     (pi1 … (joint_if_entry … p))
+     (pi1 … (joint_if_exit … p)).
+>graph_code_has_point whd in match code; >mem_set_add
+@orb_Prop_r [elim (joint_if_entry ???) | elim (joint_if_exit ???) ]
+#x #H <graph_code_has_point @H
+qed. 
 
 definition set_locals ≝

src/joint/TranslateUtils_paolo.ma

@@ -5 +5 @@
 (* type T is the syntactic type of the generated things *)
 (* (sig for RTLabs registers, unit in others ) *)
-definition freshT ≝ λg.λpars : params.λX,T : Type[0].
-   T → state_monad (joint_internal_function … g pars) X.
+definition freshT ≝ λg.λpars : params.state_monad (joint_internal_function … g pars).
 
 definition rtl_ertl_fresh_reg: 
  ∀inst_pars,funct_pars,globals.
-  freshT globals (rtl_ertl_params inst_pars funct_pars) register unit ≝
-  λinst_pars,var_pars,globals,it,def.
+  freshT globals (rtl_ertl_params inst_pars funct_pars) register ≝
+  λinst_pars,var_pars,globals,def.
     let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
     〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉.
 
+include alias "basics/lists/list.ma".
 let rec rtl_ertl_fresh_regs inst_pars funct_pars globals (n : ℕ) on n :
-  freshT globals (rtl_ertl_params inst_pars funct_pars) (list register) unit ≝
-  match n with
-  [ O ⇒ λ_. return [ ]
-  | S n' ⇒ λ_.
-    ! regs' ← rtl_ertl_fresh_regs inst_pars funct_pars globals n' it;
-    ! reg ← rtl_ertl_fresh_reg inst_pars funct_pars globals it;
-    return (reg :: regs')
-  ].
-
-lemma rtl_ertl_fresh_regs_length:
- ∀i_pars,f_pars,globals.∀def: joint_internal_function … globals
-  (rtl_ertl_params i_pars f_pars). ∀n: nat.
-  |(\snd (rtl_ertl_fresh_regs … n it def))| = n.
- #ipars#fpars #globals #def #n elim n
-  [ %
-  | #m whd in ⊢ (? → ??(??(???%))?); @pair_elim
-    #def' #regs #EQ>EQ
-    whd in ⊢ (? → ??(??(???%))?); @pair_elim #def'' #reg #_ normalize // ]
-qed.
-
-definition rtl_ertl_fresh_regs_strong:
- ∀i_pars,f_pars,globals. joint_internal_function … globals (rtl_ertl_params i_pars f_pars) →
-  ∀n: nat. Σregs: (joint_internal_function … globals (rtl_ertl_params i_pars f_pars)) × (list register). |\snd regs| = n ≝
- λi_pars,f_pars,globals,def,n.rtl_ertl_fresh_regs i_pars f_pars globals n it def. //
-qed.
+  freshT globals (rtl_ertl_params inst_pars funct_pars)
+    (Σl : list register. |l| = n) ≝
+  let ret_type ≝ (Σl : list register. |l| = n) in
+  match n  return λx.x = n → freshT … ret_type with
+  [ O ⇒ λeq'.return (mk_Sig … [ ] ?)
+  | S n' ⇒ λeq'.
+    ! regs' ← rtl_ertl_fresh_regs inst_pars funct_pars globals n';
+    ! reg ← rtl_ertl_fresh_reg inst_pars funct_pars globals;
+    return (mk_Sig … (reg :: regs') ?)
+  ](refl …). <eq' normalize [//] elim regs' #l #eql >eql //
+  qed.
 
 definition fresh_label:
- ∀g_pars,globals.freshT globals g_pars label unit ≝
-  λg_pars,globals,it,def.
+ ∀g_pars,globals.freshT globals g_pars label ≝
+  λg_pars,globals,def.
     let 〈r,luniverse〉 ≝ fresh … (joint_if_luniverse … def) in
      〈set_luniverse … def luniverse, r〉.
@@ -52 +38 @@
   (g_pars: graph_params)
   (globals: list ident)
-  (insts: list (joint_instruction g_pars globals))
+  (insts: list (joint_step g_pars globals))
   (src : label)
   (dest : label)
@@ -63 +49 @@
       add_graph … src (sequential … instr dest) def
     | _ ⇒ (* need to generate label *)
-      let 〈def, tmp_lbl〉 ≝ fresh_label … it def in
+      let 〈def, tmp_lbl〉 ≝ fresh_label … def in
       adds_graph g_pars globals others tmp_lbl dest
         (add_graph … src (sequential … instr tmp_lbl) def)
@@ -72 +58 @@
   ∀g_pars: graph_params.
   ∀globals: list ident.
-  (* type of allocatable registers and of their types (unit if not in RTLabs) *)
-  ∀R,T : Type[0].
   (* fresh register creation *)
-  freshT globals g_pars R T →
-  ∀insts: bind_list R T (joint_instruction g_pars globals).
+  freshT globals g_pars (localsT … g_pars) →
+  ∀insts: bind_list (localsT … g_pars) (joint_step g_pars globals).
   ∀src : label.
   ∀dest : label.
   joint_internal_function globals g_pars →
   joint_internal_function globals g_pars ≝
-  λg_pars,globals,T,R,fresh_r,insts,src,dest,def.
+  λg_pars,globals,fresh_r,insts,src,dest,def.
   let 〈def', stmts〉 ≝ bcompile … fresh_r insts def in
   adds_graph … stmts src dest def'.
@@ -89 +73 @@
   ∀src_g_pars,dst_g_pars : graph_params.
   ∀globals: list ident.
-  (* type of allocatable registers (unit if not in RTLabs) *)
-  ∀T : Type[0].
   (* fresh register creation *)
-  freshT globals dst_g_pars (localsT dst_g_pars) T →
+  freshT globals dst_g_pars (localsT dst_g_pars) →
   (* function dictating the translation *)
-  (label → joint_instruction src_g_pars globals →
-    bind_list (localsT dst_g_pars) T (joint_instruction dst_g_pars globals)
+  (label → joint_step src_g_pars globals →
+    bind_list (localsT dst_g_pars) (joint_step dst_g_pars globals)
     (* this can be added to allow redirections: × label *)) →
-  (label → ext_fin_instruction src_g_pars →
-    (bind_list (localsT dst_g_pars) T (joint_instruction dst_g_pars globals))
-    ×
-    (joint_statement dst_g_pars globals)) →
+  (label → ext_fin_stmt src_g_pars →
+     bind_new (localsT dst_g_pars)
+      ((list (joint_step dst_g_pars globals))
+      ×
+      (joint_statement dst_g_pars globals))) →
   (* initialized function definition with empty graph *)
   joint_internal_function globals dst_g_pars →
@@ -107 +90 @@
   (* destination function *)
   joint_internal_function globals dst_g_pars ≝ 
-  λsrc_g_pars,dst_g_pars,globals,registerT,fresh_reg,trans,trans',empty,def.
+  λsrc_g_pars,dst_g_pars,globals,fresh_reg,trans,trans',empty,def.
   let f : label → joint_statement (src_g_pars : params) globals →
     joint_internal_function globals dst_g_pars → joint_internal_function globals dst_g_pars ≝ 
@@ -115 +98 @@
     | GOTO next ⇒ add_graph … lbl (GOTO … next) def
     | RETURN ⇒ add_graph … lbl (RETURN …) def
-    | extension_fin c ⇒ let 〈l, fin〉 ≝ trans' lbl c in
-      let 〈def, tmp_lbl〉 ≝ fresh_label … it def in
-      b_adds_graph … fresh_reg l lbl tmp_lbl (add_graph … tmp_lbl fin def)
+    | extension_fin c ⇒
+      let 〈def', p〉 ≝ bcompile … fresh_reg (trans' lbl c) def in
+      let 〈insts, fin〉 ≝ p in
+      let 〈def'', tmp_lbl〉 ≝ fresh_label … def' in
+      adds_graph … insts lbl tmp_lbl (add_graph … tmp_lbl fin def)
     ] in
   foldi … f (joint_if_code … def) empty.
-
-definition b_graph_translate_no_fin :
-  ∀src_g_pars : graph_params.
-  ext_fin_instruction src_g_pars = void →
-  ∀dst_g_pars : graph_params.
-  ∀globals: list ident.
-  (* type of allocatable registers (unit if not in RTLabs) *)
-  ∀T : Type[0].
-  (* fresh register creation *)
-  freshT globals dst_g_pars (localsT dst_g_pars) T →
-  (* function dictating the translation *)
-  (label → joint_instruction src_g_pars globals →
-    bind_list (localsT dst_g_pars) T (joint_instruction dst_g_pars globals)
-    (* this can be added to allow redirections: × label *)) →
-  (* initialized function definition with empty graph *)
-  joint_internal_function globals dst_g_pars →
-  (* source function *)
-  joint_internal_function globals src_g_pars →
-  (* destination function *)
-  joint_internal_function globals dst_g_pars ≝ 
-  λsrc_g_pars,src_g_pars_prf,dst_g_pars,globals,registerT,fresh_reg,trans.
-    b_graph_translate src_g_pars dst_g_pars globals registerT fresh_reg
-      trans (λ_.λc.⊥). >src_g_pars_prf in c; #H elim H qed.
   
 (* translation without register allocation *)
@@ -149 +111 @@
   ∀globals: list ident.
   (* function dictating the translation *)
-  (label → joint_instruction src_g_pars globals →
-    list (joint_instruction dst_g_pars globals)) →
-  (label → ext_fin_instruction src_g_pars →
-    (list (joint_instruction dst_g_pars globals))
+  (label → joint_step src_g_pars globals →
+    list (joint_step dst_g_pars globals)) →
+  (label → ext_fin_stmt src_g_pars →
+    (list (joint_step dst_g_pars globals))
     ×
     (joint_statement dst_g_pars globals)) →
@@ -171 +133 @@
     | RETURN ⇒ add_graph … lbl (RETURN …) def
     | extension_fin c ⇒ let 〈l, fin〉 ≝ trans' lbl c in
-      let 〈def, tmp_lbl〉 ≝ fresh_label … it def in
+      let 〈def, tmp_lbl〉 ≝ fresh_label … def in
       adds_graph … l lbl tmp_lbl (add_graph … tmp_lbl fin def)
     ] in
   foldi ??? f (joint_if_code ?? def) empty.
+
+definition graph_to_lin_statement :
+  ∀p : unserialized_params.∀globals.
+  joint_statement (mk_graph_params p) globals → joint_statement (mk_lin_params p) globals ≝
+  λp,globals,stmt.match stmt return λ_.joint_statement (mk_lin_params p) globals with
+  [ sequential c _ ⇒ sequential … c it
+  | GOTO l ⇒ GOTO … l
+  | RETURN ⇒ RETURN …
+  | extension_fin c ⇒ extension_fin … c
+  ].
+
+lemma graph_to_lin_labels :
+  ∀p : unserialized_params.∀globals,s.
+  stmt_labels … (graph_to_lin_statement p globals s) =
+  stmt_explicit_labels … s.
+#p#globals * //
+qed.
+
+(* in order to make the coercion from lists to sets to work, one needs these hints *)
+unification hint 0 ≔ ;
+X ≟ identifier LabelTag
+⊢
+list label ≡ list X.
+
+unification hint 0 ≔ ;
+X ≟ identifier RegisterTag
+⊢
+list register ≡ list X.
+
+   
+definition hide_prf : ∀P : Prop.P → P ≝ λP,prf.prf.
+definition hide_Prop : Prop → Prop ≝ λP.P.
+
+interpretation "hide proof" 'hide p = (hide_prf ? p).
+interpretation "hide Prop" 'hide p = (hide_Prop p).
+
+(* discard all elements failing test, return first element succeeding it *)
+(* and the rest of the list, if any. *)
+let rec chop A (test : A → bool) (l : list A) on l : option (A × (list A)) ≝
+  match l with
+  [ nil ⇒ None ?
+  | cons x l' ⇒ if test x then return 〈x, l'〉 else chop A test l'
+  ].
+
+lemma chop_hit : ∀A,f,l,pr. chop A f l = Some ? pr →
+  let x ≝ \fst pr in
+  let post ≝ \snd pr in
+  ∃pre.All ? (λx.Not (bool_to_Prop (f x))) pre ∧ l = pre @ x :: post ∧ bool_to_Prop (f x).
+#A#f#l elim l
+[ normalize * #x #post #EQ destruct
+| #y #l' #Hi * #x #post
+  normalize elim (true_or_false_Prop (f y)) #fy >fy normalize
+  #EQ
+  [ destruct >fy %{[ ]} /3 by refl, conj, I/
+  | elim (Hi … EQ) #pre ** #prefalse #chopd #fx
+    %{(y :: pre)} %[%[%{fy prefalse}| >chopd %]|@fx]
+  ]
+]
+qed.
+
+lemma chop_miss : ∀A,f,l. chop A f l = None ? → All A (λx.Not (bool_to_Prop (f x))) l.
+#A#f#l elim l
+[ normalize #_ %
+| #y #l' #Hi normalize
+  elim (true_or_false_Prop (f y)) #fy >fy normalize
+  #EQ
+  [ destruct
+  | /3 by conj, nmk/
+  ]
+]
+qed.
+
+unification hint 0 ≔ p, globals;
+lp ≟ lin_params_to_params p,
+sp ≟ stmt_pars lp,
+js ≟ joint_statement sp globals,
+lo ≟ labelled_obj LabelTag js
+(*----------------------------*)⊢
+list lo ≡ codeT lp globals.
+
+definition graph_visit_ret_type ≝ λp,globals.λg : codeT (mk_graph_params p) globals.
+  λentry : label.
+  (Σ〈visited'   : identifier_map LabelTag ℕ,
+   required'  : identifier_set LabelTag,
+   generated' : codeT (mk_lin_params p) globals〉.'hide (
+      And (And (And (lookup ?? visited' entry = Some ? 0) (required' ⊆ visited'))
+        (code_forall_labels … (λl.bool_to_Prop (l∈required')) generated'))
+        (∀l,n.lookup ?? visited' l = Some ? n →
+          And (code_has_label … (rev ? generated') l)
+            (∃s.And (And
+              (lookup … g l = Some ? s)
+              (nth_opt … n (rev … generated') = Some ? 〈Some ? l, graph_to_lin_statement … s〉))
+              (opt_All ?
+                (λnext.Or (lookup … visited' next = Some ? (S n))
+                  (nth_opt … (S n) (rev … generated') = Some ? 〈None ?, GOTO … next〉))
+                (stmt_implicit_label … s)))))).
+                
+unification hint 0 ≔ tag ⊢ identifier_set tag ≡ identifier_map tag unit.
+
+let rec graph_visit
+  (p : unserialized_params)
+  (globals: list ident)
+  (g : codeT (mk_graph_params p) globals)
+  (* = graph (joint_statement (mk_graph_params p) globals *)
+  (required: identifier_set LabelTag)
+  (visited: identifier_map LabelTag ℕ) (* the reversed index of labels in the new code *)
+  (generated: codeT (mk_lin_params p) globals)
+  (* ≝ list ((option label)×(joint_statement (mk_lin_params p) globals)) *)
+  (visiting: list label)
+  (gen_length : ℕ)
+  (n: nat)
+  (entry : label)
+  (g_prf : code_closed … g)
+  (required_prf1 : ∀i.i∈required → Or (In ? visiting i) (bool_to_Prop (i ∈ visited)))
+  (required_prf2 : code_forall_labels … (λl.bool_to_Prop (l ∈ required)) generated)
+  (generated_prf1 : ∀l,n.lookup … visited l = Some ? n → hide_Prop (
+    And (code_has_label … (rev ? generated) l)
+    (∃s.And (And
+      (lookup … g l = Some ? s)
+      (nth_opt ? n (rev … generated) = Some ? 〈Some ? l, graph_to_lin_statement … s〉))
+      (opt_All ? (λnext.match lookup … visited next with
+                     [ Some n' ⇒ Or (n' = S n) (nth_opt ? (S n) (rev ? generated) = Some ? 〈None ?, GOTO … next〉)
+                     | None ⇒ And (nth_opt ? 0 visiting = Some ? next) (S n = gen_length) ]) (stmt_implicit_label … s)))))
+  (generated_prf2 : ∀l.lookup … visited l = None ? → does_not_occur … l (rev ? generated))
+  (visiting_prf : All … (λl.lookup … g l ≠ None ?) visiting)
+  (gen_length_prf : gen_length = length ? generated)
+  (entry_prf : Or (And (And (visiting = [entry]) (gen_length = 0)) (Not (bool_to_Prop (entry∈visited))))
+                  (lookup … visited entry = Some ? 0))
+  (n_prf : le (id_map_size … g) (plus n (id_map_size … visited)))
+  on n
+  : graph_visit_ret_type … g entry ≝
+  match chop ? (λx.¬x∈visited) visiting
+  return λx.chop ? (λx.¬x∈visited) visiting = x → graph_visit_ret_type … g entry with
+  [ None ⇒ λeq_chop.
+    let H ≝ chop_miss … eq_chop in
+    mk_Sig … 〈visited, required, generated〉 ?
+  | Some pr ⇒ λeq_chop.
+    let vis_hd ≝ \fst pr in
+    let vis_tl ≝ \snd pr in
+    let H ≝ chop_hit ???? eq_chop in
+    match n return λx.x = n → graph_visit_ret_type … g entry with
+    [ O ⇒ λeq_n.⊥
+    | S n' ⇒ λeq_n.
+      (* add the label to the visited ones *)
+      let visited' ≝ add … visited vis_hd gen_length in
+      (* take l's statement *)
+      let statement ≝ opt_safe … (lookup ?? g vis_hd) (hide_prf ? ?) in  
+      (* translate it to its linear version *)
+      let translated_statement ≝ graph_to_lin_statement p globals statement in
+      (* add the translated statement to the code (which will be reversed later) *)
+      let generated' ≝ 〈Some … vis_hd, translated_statement〉 :: generated in
+      let required' ≝ stmt_explicit_labels … statement ∪ required in
+      (* put successors in the visiting worklist *)
+      let visiting' ≝ stmt_labels … statement @ vis_tl in
+      (* finally, check the implicit successor *)
+      (* if it has been already visited, we need to add a GOTO *)
+      let add_req_gen ≝ match stmt_implicit_label … statement with
+        [ Some next ⇒
+          if next ∈ visited' then 〈1, {(next)}, [〈None label, GOTO … next〉]〉 else 〈0, ∅, [ ]〉
+        | None ⇒ 〈0, ∅, [ ]〉
+        ] in
+      graph_visit ???
+        (\snd (\fst add_req_gen) ∪ required')
+        visited'
+        (\snd add_req_gen @ generated')
+        visiting'
+        (\fst (\fst add_req_gen) + S(gen_length))
+        n' entry g_prf ????????
+    ] (refl …)
+  ] (refl …).
+whd
+[ (* base case, visiting is all visited *)
+  %[
+    %[
+      %[
+        elim entry_prf
+        [ ** #eq_visiting #gen_length_O #entry_vis >eq_visiting in H; * >entry_vis
+          * #ABS elim (ABS I)
+        | //
+        ]
+      | #l #l_req
+        elim (required_prf1 … l_req) #G
+        [ lapply (All_In … H G) #H >(notb_false ? H) %
+        | assumption
+        ]
+      ]
+    | assumption
+    ]
+   | #l #n #H elim (generated_prf1 … H)
+      #H1 * #s ** #H2 #H3 #H4
+      % [assumption] %{s} %
+      [% assumption
+      | @(opt_All_mp … H4) -l #l
+        lapply (in_map_domain … visited l)
+        elim (true_or_false (l∈visited)) #l_vis >l_vis
+        normalize nodelta [ * #n' ] #EQlookup >EQlookup
+        normalize nodelta *
+        [ #EQn' % >EQn' %
+        | #H %2{H}
+        | #H' lapply (All_nth … H … H') >l_vis * #ABS elim (ABS I)
+        ]
+      ]
+    ]
+|*: (* unpack H in all other cases *) elim H #pre ** #H1 #H2 #H3 ]
+(* first, close goals where add_gen_req plays no role *)
+[10: (* vis_hd is in g *) @(All_split … visiting_prf … H2)
+|1: (* n = 0 absrud *)
+  @(absurd … n_prf)
+  @lt_to_not_le
+  <eq_n
+  lapply (add_size … visited vis_hd 0 (* dummy value *))
+  >(notb_true … H3)
+  whd in match (if ? then ? else ?);
+  whd in match (? + ?);
+  whd in match (lt ? ?);
+  #EQ <EQ @subset_card @add_subset
+  [ @(All_split ? (λx.bool_to_Prop (x∈g)) ????? H2) @(All_mp … visiting_prf)
+    #a elim g #gm whd in ⊢ (?→?%); #H >(opt_to_opt_safe … H) %
+  | #l #H lapply (mem_map_domain … H) -H #H lapply(opt_to_opt_safe … H)
+    generalize in match (opt_safe ???); #n #l_is_n
+    elim (generated_prf1 … l_is_n) #_ * #s ** #s_in_g #_ #_ lapply s_in_g -s_in_g
+    elim g #mg  whd in ⊢ (?→?%); #H >H whd %
+  ]
+|6:
+  @All_append
+  [ @(g_prf … vis_hd) <opt_to_opt_safe %
+  | >H2 in visiting_prf;
+    #H' lapply (All_append_r … H') -H' * #_ //
+  ]
+|8:
+  %2 elim entry_prf
+  [ ** >H2 cases pre
+    [2: #x' #pre' #ABS normalize in ABS; destruct(ABS)
+      cases pre' in e0; [2: #x'' #pre''] #ABS' normalize in ABS'; destruct(ABS')
+    |1: #EQ normalize in EQ; destruct(EQ) #eq_gen_length #_
+      >lookup_add_hit >eq_gen_length %
+    ]
+  | #lookup_entry cut (entry ≠ vis_hd)
+    [ % whd in match vis_hd; #entry_vis_hd <entry_vis_hd in H3; #entry_vis
+      lapply (in_map_domain … visited entry) >(notb_true … entry_vis)
+      normalize nodelta >lookup_entry #ABS destruct(ABS)]
+    #entry_not_vis_hd >(lookup_add_miss ?????? entry_not_vis_hd) assumption
+  ]
+|9:
+  >commutative_plus
+  >add_size >(notb_true … H3) normalize nodelta
+  whd in match (? + ?);
+  >commutative_plus
+  change with (? ≤ S(?) + ?)
+  >eq_n assumption
+|*: (* where add_gen_req does matter, expand the three possible cases *)
+  lapply (refl … add_req_gen)
+  whd in ⊢ (???%→?);
+  lapply (refl … (stmt_implicit_label … statement))
+  (* BUG *)
+  [ generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%);
+  | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%);
+  | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%);
+  | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%);
+  | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%);
+  ]
+  *[2,4,6,8,10: #next]
+  #EQimpl
+  whd in ⊢ (???%→?);
+  [1,2,3,4,5: elim (true_or_false_Prop … (next∈visited')) #next_vis >next_vis
+    whd in ⊢ (???%→?);]
+  #EQ_req_gen >EQ_req_gen
+  (* these are the cases, reordering them *)
+  [1,2,11: | 3,4,12: | 5,6,13: | 7,8,14: |9,10,15: ]
+  [1,2,3: #i >mem_set_union
+    [ #H elim (orb_Prop_true … H) -H
+      [ #H >(mem_set_singl_to_eq … H) %2{next_vis}]
+    |*: >mem_set_empty whd in match (false ∨ ?);
+    ]
+    >mem_set_union
+    #H elim(orb_Prop_true … H) -H
+    [1,3,5: (* i is an explicit successor *)
+      #i_succ
+      (* if it's visited it's ok *)
+      elim(true_or_false_Prop (i ∈visited')) #i_vis >i_vis
+      [1,3,5: %2 %
+      |*: %
+        @Exists_append_l
+        whd in match (stmt_labels ???);
+        @Exists_append_r
+        @mem_list_as_set
+        @i_succ
+      ]
+    |2,4,6: (* i was already required *)
+      #i_req
+      elim (required_prf1 … i_req)
+      [1,3,5: >H2 #H elim (Exists_append … H) -H
+        [1,3,5: (* i in preamble → i∈visited *)
+          #i_pre %2 >mem_set_add @orb_Prop_r
+          lapply (All_In … H1 i_pre)
+          #H >(notb_false … H) %
+        |*: *
+          [1,3,5: (* i is vis_hd *)
+            #eq_i >eq_i %2 @mem_set_add_id
+          |*: (* i in vis_tl → i∈visiting' *)
+            #i_post % @Exists_append_r assumption
+          ]
+        ]
+      |*: #i_vis %2 >mem_set_add @orb_Prop_r assumption
+      ]
+    ]
+  |4,5,6:
+    [% [ whd % [ >mem_set_union >mem_set_add_id % | %]]]
+    whd in match (? @ ?); %
+    [1,3,5:
+      whd
+      >graph_to_lin_labels
+      change with (All ?? (stmt_explicit_labels ?? statement))
+      whd in match required';
+      generalize in match (stmt_explicit_labels … statement);
+      #l @list_as_set_All
+      #i >mem_set_union >mem_set_union
+      #i_l @orb_Prop_r @orb_Prop_l @i_l
+    |*: @(All_mp … required_prf2)
+      * #l_opt #s @All_mp
+      #l #l_req >mem_set_union @orb_Prop_r
+      >mem_set_union @orb_Prop_r @l_req
+    ]
+  |7,8,9:
+    #i whd in match visited';
+    @(eq_identifier_elim … i vis_hd)
+    [1,3,5: #EQi >EQi #pos
+      >lookup_add_hit #EQpos cut (gen_length = pos)
+        [1,3,5: (* BUG: -graph_visit *) -visited destruct(EQpos) %]
+        -EQpos #EQpos <EQpos -pos
+      %
+      [1,3,5: whd in match (rev ? ?);
+        >rev_append_def
+        whd
+        [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
+          <associative_append >occurs_exactly_once_None]
+        >occurs_exactly_once_Some_eq >eq_identifier_refl
+        normalize nodelta
+        @generated_prf2
+        lapply (in_map_domain … visited vis_hd)
+        >(notb_true … H3) normalize nodelta //
+      |*: %{statement}
+        %
+        [1,3,5: %
+          [1,3,5:
+           change with (? = Some ? (opt_safe ???))
+           @opt_safe_elim #s //
+          |*: whd in match (rev ? ?);
+            >rev_append_def
+            [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
+              <associative_append @nth_opt_append_hit_l ]
+            >nth_opt_append_r
+            >rev_length
+            <gen_length_prf
+            [1,3,5: <minus_n_n] %
+          ]
+        |*: >EQimpl whd [3: %]
+          >mem_set_add in next_vis;
+          @eq_identifier_elim
+          [1,3: #EQnext >EQnext * [2: #ABS elim(ABS I)]
+            >lookup_add_hit
+          |*: #NEQ >(lookup_add_miss … visited … NEQ)
+            whd in match (false ∨ ?);
+            #next_vis lapply(in_map_domain … visited next) >next_vis
+            whd in ⊢ (% → ?); [ * #s ]
+            #EQlookup >EQlookup
+          ] whd
+          [1,2: %2
+            >rev_append >nth_opt_append_r
+            >rev_length whd in match generated';
+            whd in match (|? :: ?|); <gen_length_prf
+            [1,3: <minus_n_n ] %
+          |*: % [2: %] @nth_opt_append_hit_l whd in match (stmt_labels … statement);
+            >EQimpl %
+          ]
+        ]
+      ]
+    |*:
+      #NEQ #n_i >(lookup_add_miss … visited … NEQ)
+      #Hlookup elim (generated_prf1 … Hlookup)
+      #G1 * #s ** #G2 #G3 #G4
+      %
+      [1,3,5: whd in match (rev ??);
+        >rev_append_def whd
+        [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
+          <associative_append >occurs_exactly_once_None]
+        >occurs_exactly_once_Some_eq
+        >eq_identifier_false
+        [2,4,6: % #ABS >ABS in NEQ; * #ABS' @ABS' %]
+        normalize nodelta
+        assumption
+      |*: %{s}
+        %
+        [1,3,5: %
+          [1,3,5: assumption
+          |*: whd in match (rev ??); >rev_append_def
+            [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
+              <associative_append @nth_opt_append_hit_l ]
+            @nth_opt_append_hit_l assumption
+          ]
+        |*: @(opt_All_mp … G4)
+          #x
+          @(eq_identifier_elim … x vis_hd) #Heq
+          [1,3,5: >Heq 
+            lapply (in_map_domain … visited vis_hd)
+            >(notb_true … H3)
+           normalize nodelta #EQlookup >EQlookup normalize nodelta
+           * #nth_opt_visiting #gen_length_eq
+           >lookup_add_hit normalize nodelta %
+           >gen_length_eq %
+          |*: >(lookup_add_miss ?????? Heq)
+            lapply (in_map_domain … visited x)
+            elim (true_or_false_Prop (x∈visited)) #x_vis >x_vis normalize nodelta
+            [1,3,5: * #n'] #EQlookupx >EQlookupx normalize nodelta *
+            [1,3,5: #G %{G}
+            |2,4,6: #G %2 whd in match (rev ??); >rev_append_def
+              [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
+              <associative_append @nth_opt_append_hit_l ]
+              @nth_opt_append_hit_l assumption
+            |*: #G elim(absurd ?? Heq)
+              (* BUG (but useless): -required -g -generated *)
+               >H2 in G; #G
+              lapply (refl … (nth_opt ? 0 pre))
+              (* BUG *)
+              [generalize in ⊢ (???%→?);
+              |generalize in ⊢ (???%→?);
+              |generalize in ⊢ (???%→?);
+              ] *
+              [1,3,5: #G' >(nth_opt_append_miss_l … G') in G;
+                change with (Some ? vis_hd = ? → ?)
+                #EQvis_hd' destruct(EQvis_hd') %
+              |*: #lbl'' #G' >(nth_opt_append_hit_l ? pre ??? G') in G;
+                #EQlbl'' destruct(EQlbl'') lapply (All_nth … H1 … G')
+                >x_vis * #ABS elim (ABS I)
+              ]
+            ]
+          ]
+        ]
+      ]
+    ]
+  |10,11,12:
+    #i whd in match visited';
+    lapply (in_map_domain … visited' i)
+    >mem_set_add
+    elim (true_or_false_Prop (eq_identifier … vis_hd i)) #i_vis_hd
+    >eq_identifier_sym >i_vis_hd
+    [2,4,6: elim(true_or_false (i∈visited)) #i_vis >i_vis]
+    [1,3,5,7,8,9: change with ((∃_.?) → ?); * #n #EQlook >EQlook #ABS destruct(ABS)]
+    #_ #EQlookup >lookup_add_miss in EQlookup;
+    [2,4,6: % #ABS >ABS in i_vis_hd; >eq_identifier_refl *]
+    #EQlookup
+    [1,2,3: @EQlookup %]
+    whd in match (rev ??); >rev_append_def
+    [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
+              <associative_append >does_not_occur_None]
+    >(does_not_occur_Some ?????? (i_vis_hd))
+    @generated_prf2 assumption
+  |13,14,15:
+    whd in match generated'; normalize <gen_length_prf %
+  ]
+]
+qed.
+
+(* CSC: The branch compression (aka tunneling) optimization is not implemented
+   in Matita *)
+definition branch_compress 
+  ≝ λp: graph_params.λglobals.λg:codeT p globals.
+    λentry : Σl.code_has_label … g l.g.
   
-definition graph_translate_no_fin :
-  ∀src_g_pars : graph_params.
-  ext_fin_instruction src_g_pars = void →
-  ∀dst_g_pars : graph_params.
-  ∀globals: list ident.
-  (* type of allocatable registers (unit if not in RTLabs) *)
-  (* function dictating the translation *)
-  (label → joint_instruction src_g_pars globals →
-    list (joint_instruction dst_g_pars globals)
-    (* this can be added to allow redirections: × label *)) →
-  (* initialized function definition with empty graph *)
-  joint_internal_function globals dst_g_pars →
-  (* source function *)
-  joint_internal_function globals src_g_pars →
-  (* destination function *)
-  joint_internal_function globals dst_g_pars ≝ 
-  λsrc_g_pars,src_g_pars_prf,dst_g_pars,globals,trans.
-    graph_translate src_g_pars dst_g_pars globals
-      trans (λ_.λc.⊥). >src_g_pars_prf in c; #H elim H qed.
+lemma branch_compress_closed : ∀p,globals,g,l.code_closed ?? g →
+  code_closed … (branch_compress p globals g l).
+#p#globals#g#l#H @H qed.
+
+lemma branch_compress_has_entry : ∀p,globals,g,l.
+  code_has_label … (branch_compress p globals g l) l.
+#p#globals#g*#l#l_prf @l_prf qed.
+
+definition filter_labels ≝ λtag,A.λtest : identifier tag → bool.λc : list (labelled_obj tag A).
+  map ??
+    (λs. let 〈l_opt,x〉 ≝ s in
+      〈! l ← l_opt ; if test l then return l else None ?, x〉) c.
+      
+lemma does_not_occur_filter_labels :
+  ∀tag,A,test,id,c.
+    does_not_occur ?? id (filter_labels tag A test c) =
+      (does_not_occur ?? id c ∨ ¬ test id).
+#tag #A #test #id #c elim c
+[ //
+| ** [2: #lbl] #s #tl #IH
+  whd in match (filter_labels ????); normalize nodelta
+  whd in match (does_not_occur ????) in ⊢ (??%%);
+  [2: @IH]
+  normalize in match (! l ← ? ; ?); >IH
+  @(eq_identifier_elim ?? lbl id) #Heq [<Heq]
+  elim (test lbl) normalize nodelta
+  change with (eq_identifier ???) in match (instruction_matches_identifier ????);
+  [1,2: >eq_identifier_refl [2: >commutative_orb] normalize %
+  |*: >(eq_identifier_false ??? Heq) normalize nodelta %
+  ]
+]
+qed.
+
+lemma occurs_exactly_once_filter_labels :
+  ∀tag,A,test,id,c.
+    occurs_exactly_once ?? id (filter_labels tag A test c) =
+      (occurs_exactly_once ?? id c ∧ test id).
+#tag #A #test #id #c elim c
+[ //
+| ** [2: #lbl] #s #tl #IH
+  whd in match (filter_labels ????); normalize nodelta
+  whd in match (occurs_exactly_once ????) in ⊢ (??%%);
+  [2: @IH]
+  normalize in match (! l ← ? ; ?); >IH
+  >does_not_occur_filter_labels
+  @(eq_identifier_elim ?? lbl id) #Heq [<Heq]
+  elim (test lbl) normalize nodelta
+  change with (eq_identifier ???) in match (instruction_matches_identifier ????);
+  [1,2: >eq_identifier_refl >commutative_andb [ >(commutative_andb ? true) >commutative_orb | >(commutative_andb ? false)] normalize %
+  |*: >(eq_identifier_false ??? Heq) normalize nodelta %
+  ]
+]
+qed.
+
+lemma nth_opt_filter_labels : ∀tag,A,test,instrs,n.
+  nth_opt ? n (filter_labels tag A test instrs) =
+  ! 〈lopt, s〉 ← nth_opt ? n instrs ;
+  return 〈 ! lbl ← lopt; if test lbl then return lbl else None ?, s〉.
+#tag #A #test #instrs elim instrs
+[ * [2: #n'] %
+| * #lopt #s #tl #IH * [2: #n']
+  whd in match (filter_labels ????); normalize nodelta
+  whd in match (nth_opt ???) in ⊢ (??%%); [>IH] %
+]
+qed.
+
+definition linearize_code:
+ ∀p : unserialized_params.∀globals.
+  ∀g : codeT (mk_graph_params p) globals.code_closed … g →
+  ∀entry : (Σl. code_has_label … g l).
+    (Σc : codeT (mk_lin_params p) globals.
+      code_closed … c ∧
+      ∃ sigma : identifier_map LabelTag ℕ.
+      lookup … sigma entry = Some ? 0 ∧
+      ∀l,n.lookup … sigma l = Some ? n →
+        ∃s. lookup … g l = Some ? s ∧
+          opt_Exists ?
+            (λls.let 〈lopt, ts〉 ≝ ls in
+              opt_All ? (eq ? l) lopt ∧
+              ts = graph_to_lin_statement … s ∧
+              opt_All ?
+                (λnext.Or (lookup … sigma next = Some ? (S n))
+                (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
+                (stmt_implicit_label … s)) (nth_opt … n c))
+≝
+ λp,globals,g,g_prf,entry_sig.
+    let g ≝ branch_compress (mk_graph_params p) ? g entry_sig in
+    let g_prf ≝ branch_compress_closed … g entry_sig g_prf in
+    let entry_sig' ≝ mk_Sig ?? entry_sig (branch_compress_has_entry … g entry_sig) in
+    match graph_visit p globals g ∅ (empty_map …) [ ] [entry_sig] 0 (|g|)
+      (entry_sig) g_prf ????????
+    with
+    [ mk_Sig triple H ⇒ 
+      let sigma ≝ \fst (\fst triple) in
+      let required ≝ \snd (\fst triple) in
+      let crev ≝ \snd triple in
+      let lbld_code ≝ rev ? crev in
+      mk_Sig ?? (filter_labels … (λl.l∈required) lbld_code) ? ].
+[ (* done later *)
+| #i >mem_set_empty *
+| %
+|#l #n normalize in ⊢ (%→?); #ABS destruct(ABS)
+| #l #_ %
+| % [2: %] @(pi2 … entry_sig')
+| %
+| % % [% %] cases (pi1 … entry_sig) normalize #_ % //
+| >commutative_plus change with (? ≤ |g|) %
+]
+lapply (refl … triple)
+generalize in match triple in ⊢ (???%→%); **
+#visited #required #generated #EQtriple
+>EQtriple in H ⊢ %; normalize nodelta ***
+#entry_O #req_vis #labels_in_req #sigma_prop
+% >EQtriple
+[ (* code closed *)
+  @All_map
+  [2: @All_rev
+    @(All_mp … labels_in_req) #ls #H @H
+  |1: (* side-effect close *)
+  |3: * #lopt #s @All_mp
+    #lbl #lbl_req whd in match (code_has_label ????);
+    >occurs_exactly_once_filter_labels
+    @andb_Prop [2: assumption]
+    lapply (in_map_domain … visited lbl)
+    >(req_vis … lbl_req) * #n #eq_lookup
+    elim (sigma_prop ?? eq_lookup) #H #_ @H
+  ]
+]
+%{visited} % [assumption]
+#lbl #n #eq_lookup elim (sigma_prop ?? eq_lookup)
+#lbl_in_gen * #stmt ** #stmt_in_g #nth_opt_is_stmt #succ_is_in
+% [2: % [ assumption ] |]
+>nth_opt_filter_labels in ⊢ (???%);
+>nth_opt_is_stmt
+whd in match (! 〈lopt, s〉 ← Some ??; ?);
+whd
+whd in match (! lbl0 ← Some ??; ?);
+% [ % [ elim (lbl ∈ required) ] % ]
+whd
+lapply (refl … (stmt_implicit_label … stmt))
+generalize in match (stmt_implicit_label … stmt) in ⊢ (???%→%); * [2: #next]
+#eq_impl_lbl normalize nodelta [2: %]
+>eq_impl_lbl in succ_is_in; whd in match (opt_All ???); * #H
+[ %{H}
+| %2 >nth_opt_filter_labels >H
+  whd in match (! 〈lopt, s〉 ← ?; ?);
+  whd in match (! lbl0 ← ?; ?);
+  %
+]
+qed.
+
+definition graph_linearize :
+  ∀p : unserialized_params.
+  ∀globals. ∀fin : joint_closed_internal_function globals (mk_graph_params p).
+    Σfout : joint_closed_internal_function globals (mk_lin_params p).
+      ∃sigma : identifier_map LabelTag ℕ. 
+        let g ≝ joint_if_code ?? (pi1 … fin) in
+        let c ≝ joint_if_code ?? (pi1 … fout) in
+        let entry ≝ joint_if_entry ?? (pi1 … fin) in
+         lookup … sigma entry = Some ? 0 ∧
+          ∀l,n.lookup … sigma l = Some ? n →
+            ∃s. lookup … g l = Some ? s ∧
+              opt_Exists ?
+                (λls.let 〈lopt, ts〉 ≝ ls in
+                  opt_All ? (eq ? l) lopt ∧
+                  ts = graph_to_lin_statement … s ∧
+                  opt_All ?
+                    (λnext.Or (lookup … sigma next = Some ? (S n))
+                    (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
+                    (stmt_implicit_label … s)) (nth_opt … n c) ≝
+  λp,globals,f_sig.
+  mk_Sig ?? (match f_sig with
+  [ mk_Sig f f_prf ⇒  
+  mk_joint_internal_function globals (mk_lin_params p)
+   (joint_if_luniverse ?? f) (joint_if_runiverse ?? f)
+   (joint_if_result ?? f) (joint_if_params ?? f) (joint_if_locals ?? f)
+   (joint_if_stacksize ?? f)
+   (linearize_code p globals (joint_if_code … f) f_prf (joint_if_entry … f))
+   (mk_Sig ?? it I) (mk_Sig ?? it I)
+  ]) ?.
+elim f_sig
+normalize nodelta #f_in #f_in_prf
+elim (linearize_code ?????)
+#f_out * #f_out_closed #H assumption
+qed. 
+
   
 

src/joint/semanticsUtils_paolo.ma

@@ -21 +21 @@
 (******************************** GRAPHS **************************************)
 
-definition graph_pointer_of_label0:
- pointer → label → Σp:pointer. ptype p = Code ≝
- λoldpc,l.
-  mk_pointer Code
-   (mk_block Code (block_id (pblock oldpc))) ? (mk_offset (pos (word_of_identifier … l))). 
-// qed.
-
-definition graph_pointer_of_label :
-  ∀pars : graph_params.∀globals. genv globals pars → pointer → label →
-    res (Σp:pointer. ptype p = Code) ≝
- λ_.λ_.λ_.λoldpc,l.
-  OK ? (graph_pointer_of_label0 oldpc l). 
+definition graph_pointer_of_label : cpointer → label → res cpointer ≝
+  λoldpc,l.
+  return (mk_pointer Code
+   (mk_block Code (block_id (pblock oldpc))) ? (mk_offset (pos (word_of_identifier … l))) : cpointer). 
+% qed.
 
 definition graph_label_of_pointer: pointer → res label ≝
  λp. OK … (an_identifier ? (match offv (poff p) with [ OZ ⇒ one | pos x ⇒ x | neg x ⇒ x ])).
-
-(*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label.
- But I can't use it directly because this one uses a concrete definition of
- pointer_of_label and it is used to istantiate the more_sem_params record
- where the abstract version is declared as a field. Is there a better way
- to organize the code? *)
-definition graph_succ_p: label → address → res address ≝
- λl,old.
-  do ptr ← pointer_of_address old ;
-  let newptr ≝ graph_pointer_of_label0 ptr l in
-  address_of_pointer newptr.
 
 definition graph_fetch_statement:
@@ -53 +35 @@
  ∀globals.
   genv globals pars →
-  state sem_pars →
+  cpointer →
   res (joint_statement pars globals) ≝
- λpars,sem_pars,globals,ge,st.
-  do p ← code_pointer_of_address (pc … st) ;
+ λpars,sem_pars,globals,ge,p.
   do f ← fetch_function … ge p ;
   do l ← graph_label_of_pointer p;
@@ -71 +52 @@
       pars
       g_pars
-      graph_succ_p
-      (graph_pointer_of_label ?)
-      (graph_fetch_statement ? ?)
+      graph_pointer_of_label
+      (λ_.λ_.graph_pointer_of_label)
+      (graph_fetch_statement ? g_pars)
     ).
     
 (******************************** LINEAR **************************************)
-
-definition lin_succ_p: unit → address → res address :=
- λ_.λaddr. addr_add addr 1.
-
+check mk_pointer
+definition lin_succ_p: cpointer → unit → res cpointer :=
+ λptr.λ_.return «mk_pointer Code (pblock ptr) ? (mk_offset (offv (poff ptr) + 1)), ?».
+[%| cases ptr //] qed.
 
 axiom BadLabel: String.
@@ -86 +67 @@
 definition lin_pointer_of_label:
  ∀pars : lin_params.
- ∀globals. genv globals pars → pointer → label →
-  res (Σp:pointer. ptype p = Code) ≝
+ ∀globals. genv globals pars → cpointer → label → res cpointer ≝
  λpars,globals,ge,old,l.
   do fn ← fetch_function … ge old ;
@@ -97 +77 @@
      (joint_if_code … pars fn)) ;
   OK … (mk_Sig … (mk_pointer Code (mk_block Code (block_id (pblock old))) ? (mk_offset pos)) ?).
-// qed.
+% qed.
 
 definition lin_fetch_statement:
@@ -103 +83 @@
  ∀sem_pars : sem_state_params.
  ∀globals.
- genv globals pars → state sem_pars → res (joint_statement pars globals) ≝
- λpars,sem_pars,globals,ge,st.
-  do ppc ← pointer_of_address (pc … st) ;
+ genv globals pars → cpointer → res (joint_statement pars globals) ≝
+ λpars,sem_pars,globals,ge,ppc.
   do fn ← fetch_function … ge ppc ;
   let off ≝ abs (offv (poff ppc)) in (* The offset should always be positive! *)
@@ -123 +102 @@
       lin_succ_p
       (lin_pointer_of_label ?)
-      (lin_fetch_statement ? ?)
+      (lin_fetch_statement ? g_pars)
     ).
     
-
+definition step_unbranching : ∀p,globals.joint_step p globals → bool ≝
+  λp,globals,stp.match stp with
+  [ COND _ _ ⇒ false
+  | CALL_ID _ _ _ ⇒ false
+  | extension c' ⇒ (* FIXME: does not care about calling extensions!! *)
+    match ext_step_labels … c' with
+    [ nil ⇒ true
+    | _ ⇒ false
+    ]
+  | _ ⇒ true
+  ].
+
+definition is_not_seq : ∀p,globals.joint_statement p globals → bool ≝
+  λp,globals,stp.match stp with
+  [ sequential _ _ ⇒ false
+  | _ ⇒ true
+  ].
+
+inductive s_block (p : params) (globals : list ident) : Type[0] ≝
+  | Skip : s_block p globals
+  | FinStep : (Σs.bool_to_Prop (¬step_unbranching p globals s)) → s_block p globals
+  | FinStmt : (Σs.bool_to_Prop (is_not_seq p globals s)) → s_block p globals
+  | Cons : (Σs.bool_to_Prop (step_unbranching p globals s)) → s_block p globals → s_block p globals.
+
+include "utilities/bind_new.ma".
+
+definition Block ≝ λp : params.λglobals.bind_new (localsT p) (s_block p globals).
+
+definition Bcons ≝ λp : params.λglobals.
+    λs : Σs.bool_to_Prop (step_unbranching p globals s).
+    λB : Block p globals.
+    ! b ← B ; return Cons ?? s b.
+
+interpretation "block cons" 'vcons hd tl = (Bcons ??? hd tl).
+
+let rec is_unbranching p globals (b1 : s_block p globals) on b1 : bool ≝
+  match b1 with
+  [ Skip ⇒ true
+  | FinStep _ ⇒ false
+  | FinStmt _ ⇒ false
+  | Cons _ tl ⇒ is_unbranching ?? tl
+  ].
+
+let rec Is_unbranching p globals (b1 : Block p globals) on b1 : Prop ≝
+  match b1 with
+  [ bret b ⇒ bool_to_Prop (is_unbranching … b)
+  | bnew f ⇒ ∀x.Is_unbranching … (f x)
+  ].
+
+let rec s_block_append_aux p globals (b1 : s_block p globals) (b2 : s_block p globals) on b1 : is_unbranching … b1 → s_block p globals ≝
+  match b1 return λx.is_unbranching ?? x → ? with
+  [ Skip ⇒ λ_.b2
+  | Cons x tl ⇒ λprf.Cons ?? x (s_block_append_aux ?? tl b2 prf)
+  | _ ⇒ Ⓧ
+  ].
+
+definition s_block_append ≝
+  λp,globals.λb1 : Σb.bool_to_Prop (is_unbranching … b).λb2.
+  match b1 with
+  [ mk_Sig b1 prf ⇒ s_block_append_aux p globals b1 b2 prf ].
+
+definition Is_to_is_unbr : ∀p,globals.(ΣB.Is_unbranching p globals B) →
+  bind_new (localsT p) (Σb.bool_to_Prop (is_unbranching p globals b)) ≝
+  λp,globals. ?.
+* #b elim b -b
+[ #b #H @bret @b @H
+| #f #IH #H @bnew #x @(IH x) @H
+]
+qed.
+
+lemma Is_to_is_unbr_OK : ∀p,globals,B.! b ← Is_to_is_unbr p globals B ; return pi1 … b = pi1 … B.
+#p #globals * #b elim b
+[ //
+| #f #IH #H @bnew_proper
+  #x @IH
+]
+qed.
+  
+definition Block_append ≝
+  λp,globals.λB : Σb.Is_unbranching … b.λB'.
+  ! b1 ← Is_to_is_unbr … B;
+  ! b2 ← B';
+  return s_block_append p globals b1 b2.
+
+definition all_unbranching ≝ λp,globals.All ? (λs.bool_to_Prop (step_unbranching p globals s)).
+
+let rec step_list_to_s_block (p : params) globals (l : list (joint_step p globals)) on l :
+    s_block p globals ≝
+  match l  with
+  [ nil ⇒ Skip ??
+  | cons hd tl ⇒
+    If step_unbranching … hd then with prf do
+      Cons ?? hd (step_list_to_s_block ?? tl)
+    else with prf do
+      FinStep ?? hd
+  ]. [assumption | >prf % ] qed.
+  
+definition step_list_to_block : ∀R,p,g.? → Block R p g ≝
+  λR,p,globals,l.bret R ? (step_list_to_s_block p globals l).
+
+record sem_rel (p1 : sem_params) (p2 : sem_params) (globals : list ident) : Type[0] ≝
+  { function_rel : joint_function globals p1 → joint_function globals p2 → Prop
+  ; genv_rel : genv globals p1 → genv globals p2 → Prop
+  ; pc_rel : cpointer → cpointer → Prop
+  ; st_rel : state p1 → state p2 → Prop
+  ; stmt_rel : joint_statement p1 globals → Block 
+  (* TODO: state what do we need of genv_rel (like finding the same symbols and what relation to above rels ) *)
+  ; st_to_pc_rel : ∀st1,st2.st_rel st1 st2 → pc_rel (pc ? st1) (pc ? st2)
+  }.
+  
+(* move *)
+definition beval_pair_of_xdata_pointer: (Σp:pointer. ptype p = XData) → beval × beval ≝
+ λp. match p return λp. ptype p = XData → ? with [ mk_pointer pty pbl pok poff ⇒
+  match pty return λpty. ? → pty = XData → ? with
+   [ XData ⇒ λpok.λE. list_to_pair ? (bevals_of_pointer (mk_pointer XData pbl ? poff)) ?
+   | _ ⇒ λpok'.λabs. ⊥] pok] ?.
+[@(pi2 … p) |6: // |7: %] destruct (abs)
+qed.
+
+definition safe_address_of_xdata_pointer: (Σp:pointer. ptype p = XData) → safe_address ≝ beval_pair_of_xdata_pointer.
+cases H -H * #r #b #H #o #EQ destruct(EQ) normalize lapply H
+lapply (pointer_compat_from_ind … H) -H cases b * #z * #H
+%{«mk_pointer ? (mk_block ? z) H o,I»}
+% [2,4: % [2,4: % [1,3: % [1,3: % ]] % |*:]|*:]
+qed.
+
+definition state_rel : ∀p1,p2.∀R : sem_rel p1 p2.good_state p1 → good_state p2 → Prop ≝
+  λp1,p2,R,st1,st2.
+    frames_rel p1 p2 R (st_frms … st1) (st_frms … st2) ∧
+    pc_rel p1 p2 R (pc … st1) (pc … st2) ∧
+    sp_rel p1 p2 R
+      (safe_address_of_xdata_pointer (sp … st1))
+      (safe_address_of_xdata_pointer (sp … st2)) ∧
+    isp_rel p1 p2 R
+      (safe_address_of_xdata_pointer (isp … st1))
+      (safe_address_of_xdata_pointer (isp … st2)) ∧
+    sp_rel p1 p2 R
+      (safe_address_of_xdata_pointer (sp … st1))
+      (safe_address_of_xdata_pointer (sp … st2)) ∧
+    carry … st1 = carry … st2 ∧
+    regs_rel p1 p2 R (regs … st1) (regs … st2) ∧
+    mem_rel p1 p2 R (m … st1) (m … st2).
+elim st1 -st1 #st1 ** #good_pc1 #good_sp1 #good_isp1
+elim st2 -st2 #st2 ** #good_pc2 #good_sp2 #good_isp2
+assumption
+qed.
+ elim st2
+-st1 -st2 #st2 ** #good_pc2 # ∧
+    frames_rel … R (st_frms … st1) (st_frms … st2) ∧
+    frames_rel … R (st_frms … st1) (st_frms … st2) ∧
+    frames_rel … R (st_frms … st1) (st_frms … st2) ∧
+
+
+

src/joint/semantics_paolo.ma

@@ -12 +12 @@
 
 definition genv ≝ λglobals.λp:params. genv_t Genv (joint_function globals p).
+definition cpointer ≝ Σp.ptype p = Code.
+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).
 
 record sem_state_params : Type[1] ≝
@@ -17 +21 @@
  ; empty_framesT: framesT
  ; regsT : Type[0]
- ; empty_regsT: address → regsT (* Stack pointer *)
+ ; empty_regsT: xpointer → regsT (* Stack pointer *)
  }.
  
 record state (semp: sem_state_params): Type[0] ≝
  { st_frms: framesT semp 
- ; pc: address
- ; sp: pointer
- ; isp: pointer
+ ; sp: xpointer
+ ; isp: xpointer
  ; carry: beval
  ; regs: regsT semp
  ; m: bemem
  }.
- 
+
+record state_pc (semp : sem_state_params) : Type[0] ≝
+  { st_no_pc :> state semp
+  ; pc : cpointer
+  }.
+
 definition set_m: ∀p. bemem → state p → state p ≝
- λp,m,st. mk_state p (st_frms … st) (pc … st) (sp … st) (isp … st) (carry … st) (regs … st) m.
+ λp,m,st. mk_state p (st_frms ?…st) (sp … st) (isp … st) (carry … st) (regs … st) m.
 
 definition set_regs: ∀p:sem_state_params. regsT p → state p → state p ≝
- λp,regs,st. mk_state p (st_frms … st) (pc … st) (sp … st) (isp … st) (carry … st) regs (m … st).
-
-definition set_sp: ∀p. pointer → state p → state p ≝
- λp,sp,st. mk_state … (st_frms … st) (pc … st) sp (isp … st) (carry … st) (regs … st) (m … st).
-
-definition set_isp: ∀p. pointer → state p → state p ≝
- λp,isp,st. mk_state … (st_frms … st) (pc … st) (sp … st) isp (carry … st) (regs … st) (m … st).
+ λp,regs,st. mk_state p (st_frms … st) (sp … st) (isp … st) (carry … st) regs (m … st).
+
+definition set_sp: ∀p. ? → state p → state p ≝
+ λp,sp,st. mk_state … (st_frms … st) sp (isp … st) (carry … st) (regs … st) (m … st).
+
+definition set_isp: ∀p. ? → state p → state p ≝
+ λp,isp,st. mk_state … (st_frms … st) (sp … st) isp (carry … st) (regs … st) (m … st).
 
 definition set_carry: ∀p. beval → state p → state p ≝
- λp,carry,st. mk_state … (st_frms … st) (pc … st) (sp … st) (isp … st) carry (regs … st) (m … st).
-
-definition set_pc: ∀p. address → state p → state p ≝
- λp,pc,st. mk_state … (st_frms … st) pc (sp … st) (isp … st) (carry … st) (regs … st) (m … st).
+ λp,carry,st. mk_state … (st_frms … st) (sp … st) (isp … st) carry (regs … st) (m … st).
+
+definition set_pc: ∀p. ? → state_pc p → state_pc p ≝
+ λp,pc,st. mk_state_pc … (st_no_pc … st) pc.
+
+definition set_no_pc: ∀p. ? → state_pc p → state_pc p ≝
+ λp,s,st. mk_state_pc … s (pc … st).
 
 definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝
- λp,frms,st. mk_state … frms (pc … st) (sp … st) (isp … st) (carry … st) (regs … st) (m … st).
+ λp,frms,st. mk_state … frms (sp … st) (isp … st) (carry … st) (regs … st) (m … st).
 
 axiom BadProgramCounter : String.
@@ -57 +68 @@
  ∀globals.
   genv globals pars →
-  pointer →
+  cpointer →
   res (joint_internal_function … pars) ≝
  λpars,globals,ge,p.
@@ -65 +76 @@
   [ Internal def' ⇒ OK … def'
   | External _ ⇒ Error … [MSG BadProgramCounter]].
-  
+
+inductive step_flow (p : params) (globals : list ident) : Type[0] ≝
+  | Redirect : label → step_flow p globals (* used for goto-like flow alteration *)
+  | Init     : Z → joint_internal_function globals p → call_args p → call_dest p → step_flow p globals (* call a function with given id, then proceed *)
+  | Proceed  : step_flow p globals. (* go to implicit successor *)
+
+inductive stmt_flow (p : params) (globals : list ident) : Type[0] ≝
+  | SRedirect : label → stmt_flow p globals
+  | SProceed : succ p → stmt_flow p globals
+  | SInit     : Z → joint_internal_function globals p → call_args p → call_dest p → succ p → stmt_flow p globals
+  | STailInit : Z → joint_internal_function globals p → call_args p → stmt_flow p globals
+  | SEnd  : stmt_flow p globals. (* end flow *)
+
+
 record more_sem_unserialized_params (uns_pars : unserialized_params) : Type[1] ≝
   { st_pars :> sem_state_params
@@ -82 +106 @@
   ; snd_arg_retrieve_ : regsT st_pars → snd_arg uns_pars → res beval
   ; pair_reg_move_ : regsT st_pars → pair_move uns_pars → res (regsT st_pars)
-  ; fetch_ra: state st_pars →
-      res ((state st_pars) × address)
-
-  ; init_locals : localsT uns_pars → regsT st_pars → regsT st_pars
+  ; fetch_ra: state st_pars → res ((state st_pars) × cpointer)
+
+  ; allocate_local : localsT uns_pars → regsT st_pars → regsT st_pars
   (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
-  ; save_frame: address → call_dest uns_pars → state st_pars → state st_pars
+  ; save_frame: cpointer → call_dest uns_pars → state st_pars → framesT st_pars
    (*CSC: setup_call returns a res only because we can call a function with the wrong number and
      type of arguments. To be fixed using a dependent type *)
@@ -94 +117 @@
   ; fetch_external_args: external_function → state st_pars →
       res (list val)
-  ; set_result: list val → state st_pars →
-      res (state st_pars)
+  ; set_result: list val → state st_pars → res (state st_pars)
   ; call_args_for_main: call_args uns_pars
   ; call_dest_for_main: call_dest uns_pars
@@ -111 +133 @@
   (∀up.∀p : more_sem_unserialized_params up.X up p → beval → regsT p → res (regsT p)) →
   ∀up.∀p : more_sem_unserialized_params up.X up p → beval → state p → res (state p) ≝
-  λX,f,up,p,x,v,st.! r ← f ? p x v (regs … st) ; return (set_regs … r st).
+  λX,f,up,p,x,v,st.! r ← f ? p x v (regs … st) ; return set_regs … r st.
 
 definition acca_retrieve ≝ helper_def_retrieve ? acca_retrieve_.
@@ -126 +148 @@
 definition dph_arg_retrieve ≝ helper_def_retrieve ? dph_arg_retrieve_.
 definition snd_arg_retrieve ≝ helper_def_retrieve ? snd_arg_retrieve_.
-definition pair_reg_move : ?→?→?→?→res ? ≝
+definition pair_reg_move : ?→?→?→?→?  ≝
   λup.λp : more_sem_unserialized_params up.λst : state p.λpm : pair_move up.
     ! r ← pair_reg_move_ ? p (regs ? st) pm;
-    return (set_regs ? r st).
-
+    return set_regs ? r st.
+
+ 
 axiom BadPointer : String.
-
+ 
 (* this is preamble to all calls (including tail ones). The optional argument in
    input tells the function whether it has to save the frame for internal
    calls.
-   the first element of the triple is the label at the start of the function
-   in case of an internal call, or None in case of an external one.
+   the first element of the triple is the entry point of the function if
+   it is an internal one, or false in case of an external one.
    The actual update of the pc is left to later, as it depends on
    serialization and on whether the call is a tail one. *)
-definition eval_call_block_preamble:
+definition eval_call_block:
  ∀globals.∀p : params.∀p':more_sem_unserialized_params p.
-  genv globals p → state p' → block → call_args p → option ((call_dest p) × address) →
-    IO io_out io_in ((option label)×trace×(state p')) ≝
- λglobals,p,p',ge,st,b,args,dest_ra.
+  genv globals p → state p' → block → call_args p → call_dest p →
+    IO io_out io_in ((step_flow p globals)×trace×(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
     [ Internal fn ⇒
-      let st ≝ match dest_ra with
-        [ Some p ⇒ let 〈dest, ra〉 ≝ p in save_frame … ra dest st
-        | None ⇒ st
-        ] in
-      ! st ← setup_call … (joint_if_stacksize … fn) (joint_if_params … fn)
-              args st ;
-      let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
-      let l' ≝ joint_if_entry … fn in
-      let st ≝ set_regs p' regs st in
-      return 〈Some label l', E0, st〉
+      return 〈Init … (block_id b) fn args dest, E0, st〉
     | External fn ⇒
       ! params ← fetch_external_args … p' fn st : IO ???;
@@ -167 +181 @@
       let vs ≝ [mk_val ? evres] in
       ! st ← set_result … p' vs st : IO ???;
-      return 〈None ?, Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉
+      return 〈Proceed ??, Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉
       ].
 
 axiom FailedStore: String.
 
-definition push: ∀p. state p → beval → res (state p) ≝
+definition push: ∀p.state p → beval → res (state p) ≝
  λp,st,v.
-  let isp ≝ isp … st in
-  do m ← opt_to_res … (msg FailedStore) (bestorev (m … st) isp v);
-  let isp ≝ shift_pointer … isp [[false;false;false;false;false;false;false;true]] in
-  OK … (set_m … m (set_isp … isp st)).
-
-definition pop: ∀p. state p → res (state p × beval) ≝
+  let isp' ≝ isp ? st in
+  do m ← opt_to_res ? (msg FailedStore) (bestorev (m … st) isp' v);
+  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) //
+qed.
+
+definition pop: ∀p. state p → res ((state p ) × beval) ≝
  λp,st.
-  let isp ≝ isp ? st in
-  let isp ≝ neg_shift_pointer ? isp [[false;false;false;false;false;false;false;true]] in
-  let ist ≝ set_isp … isp st in
-  do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp);
-  OK ? 〈st,v〉.
-
-definition save_ra : ∀p. state p → address → res (state p) ≝
+  let isp' ≝ isp ? st in
+  let isp'' ≝ neg_shift_pointer ? isp' [[false;false;false;false;false;false;false;true]] in
+  let ist ≝ set_isp … isp'' st in
+  do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp'');
+  OK ? 〈ist,v〉.
+  normalize elim (isp p st) //
+qed.
+  
+definition save_ra : ∀p. state p → cpointer → res (state p) ≝
  λp,st,l.
-  let 〈addrl,addrh〉 ≝ l in
-  do st ← push … st addrl;
-  push … st addrh.
-
-definition load_ra : ∀p.state p → res (state p × address) ≝
+  let 〈addrl,addrh〉 ≝ address_of_code_pointer l in
+  ! st' ← push … st addrl;
+  push … st' addrh.
+
+definition load_ra : ∀p.state p → res ((state p) × cpointer) ≝
  λp,st.
-  do 〈st,addrh〉 ← pop … st;
-  do 〈st,addrl〉 ← pop … st;
-  OK ? 〈st, 〈addrl,addrh〉〉.
-
+  do 〈st',addrh〉 ← pop … st;
+  do 〈st'',addrl〉 ← pop … st';
+  do pr ← code_pointer_of_address 〈addrh, addrl〉;
+  return 〈st'', pr〉.
+
+definition flow_no_seq : ∀p,g.stmt_flow p g → Prop ≝ λp,g,flow.
+  match flow with
+  [ SProceed _ ⇒ False
+  | SInit _ _ _ _ _ ⇒ False
+  | _ ⇒ True
+  ].
 
 (* parameters that need full params to have type of functions,
-   but are still independent of serialization
-   Paolo: the first element returned by exec extended is None if flow is
-   left to regular sequential one, otherwise a label.
-   The address input is the address of the next statement, to be provided to
-   accomodate extensions that make calls. *)
+   but are still independent of serialization *)
 record more_sem_genv_params (pp : params) : Type[1] ≝
   { msu_pars :> more_sem_unserialized_params pp
   ; read_result: ∀globals.genv globals pp → state msu_pars → res (list beval)
-  ; exec_extended: ∀globals.genv globals pp → ext_instruction pp →
-      state msu_pars → address → IO io_out io_in ((option label)× trace × (state msu_pars))
-  ; exec_fin_extended: ∀globals.genv globals pp → ext_fin_instruction pp →
-      state msu_pars → IO io_out io_in (trace × (state msu_pars))
+  (* change of pc must be left to *_flow execution *)
+  ; exec_extended: ∀globals.genv globals pp → ext_step pp →
+      state msu_pars →
+      IO io_out io_in ((step_flow pp globals)× trace × (state msu_pars))
+  ; exec_fin_extended: ∀globals.genv globals pp → ext_fin_stmt pp →
+      state msu_pars →
+      IO io_out io_in ((Σs.flow_no_seq pp globals s)× trace × (state msu_pars))
   ; pop_frame: ∀globals.genv globals pp → state msu_pars → res (state msu_pars)
   }.
-  
 
 (* parameters that are defined by serialization *)
 record more_sem_params (pp : params) : Type[1] ≝
   { msg_pars :> more_sem_genv_params pp
-  ; succ_pc: succ pp → address → res address
-  ; pointer_of_label: ∀globals.genv globals pp → pointer → label → res (Σp:pointer. ptype p = Code)
-  ; fetch_statement: ∀globals.genv globals pp → state msg_pars → res (joint_statement pp globals)
+  ; offset_of_point : code_point pp → offset
+  ; point_of_offset : offset → option (code_point pp)
+  ; point_of_offset_of_point : ∀pt.point_of_offset (offset_of_point pt) = Some ? pt
+  ; offset_of_point_of_offset : ∀o.opt_All ? (eq ? o) (! pt ← point_of_offset o ; return offset_of_point pt)
   }.
+
+definition pointer_of_point : ∀p.more_sem_params p →
+  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.
+
+axiom BadOffsetForCodePoint : String.
+
+definition point_of_pointer :
+  ∀p.more_sem_params p → cpointer → res (code_point p) ≝
+  λp,msp,ptr.opt_to_res … (msg BadOffsetForCodePoint)
+    (point_of_offset p msp (poff ptr)).
+
+lemma point_of_pointer_of_point :
+  ∀p,msp.∀ptr : cpointer.∀pt.point_of_pointer p msp (pointer_of_point p msp ptr pt) = return pt.
+#p #msp #ptr #pt normalize
+>point_of_offset_of_point %
+qed.
+
+lemma pointer_of_point_block :
+  ∀p,msp,ptr,pt.pblock (pointer_of_point p msp ptr pt) = pblock ptr.
+/ by refl/
+qed.
+
+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
+#pt #EQ3 destruct normalize //
+qed.
+
+lemma pointer_of_point_of_pointer :
+  ∀p,msp.∀ptr1,ptr2 : cpointer.∀pt.
+    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
+destruct
+lapply (offset_of_point_of_offset p msp o1)
+normalize
+elim (point_of_offset ???) normalize [* #ABS destruct(ABS)]
+#pt' #EQ #EQ' destruct %
+qed.
+
+
+axiom ProgramCounterOutOfCode : String.
+axiom PointNotFound : String.
+axiom LabelNotFound : String.
+
+definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals.
+  genv globals p → cpointer → res (joint_statement p globals) ≝
+  λp,msp,globals,ge,ptr.
+  ! pt ← point_of_pointer ? msp ptr ;
+  ! fn ← fetch_function … ge ptr ;
+  opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt).
+
+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 pointer_of_point ? msp ptr pt.
+
+definition succ_pc : ∀p : params.∀ msp : more_sem_params p.
+  cpointer → succ p → res cpointer ≝
+  λp,msp,ptr,nxt.
+  ! curr ← point_of_pointer p msp ptr ;
+  return pointer_of_point p msp ptr (point_of_succ p curr nxt).  
 
 record sem_params : Type[1] ≝
@@ -230 +325 @@
   }.
 
-definition address_of_label: ∀globals. ∀p:sem_params.
+(* definition address_of_label: ∀globals. ∀p:sem_params.
   genv globals p → pointer → label → res address ≝
  λglobals,p,ge,ptr,l.
   do newptr ← pointer_of_label … p ? ge … ptr l ;
-  OK … (address_of_code_pointer newptr).
+  OK … (address_of_code_pointer newptr). *)
 
 definition goto: ∀globals. ∀p:sem_params.
-  genv globals p → label → state p → res (state p) ≝
+  genv globals p → label → state_pc p → res (state_pc p) ≝
  λglobals,p,ge,l,st.
-  ! oldpc ← pointer_of_address (pc … st);
-  ! newpc ← address_of_label … ge oldpc l ;
-  OK (state p) (set_pc … newpc st).
+  ! newpc ← pointer_of_label ? p … ge (pc … st) l ;
+  return set_pc … newpc st.
 
 (*
@@ -248 +342 @@
 *)
 
-definition next: ∀p:sem_params. succ … p → state p → res (state p) ≝
+definition next : ∀p : sem_params.succ p → state_pc p → res (state_pc p) ≝
  λp,l,st.
-  ! l' ← succ_pc … p l (pc … st) ;
-  OK … (set_pc … l' st).
+ ! nw ← succ_pc ? p … (pc ? st) l ;
+ return set_pc … nw st.
 
 axiom MissingSymbol : String.
 axiom FailedLoad : String.
 axiom BadFunction : String.
-
-definition eval_call_block:
+axiom SuccessorNotProvided : String.
+
+(* the optional point must be given only for calls *)
+definition eval_step :
  ∀globals.∀p:sem_params. genv globals p → state p →
-  block → call_args p → call_dest p → address → IO io_out io_in (trace×(state p)) ≝
- λglobals,p,ge,st,b,args,dest,ra.
- ! 〈next, tr, st〉 ← eval_call_block_preamble … ge st b args (Some ? 〈dest,ra〉) ;
- ! new_pc ← match next with
-  [ Some lbl ⇒
-    let pointer_in_fn ≝ mk_pointer Code (mk_block Code (block_id b)) ? (mk_offset 0) in
-    address_of_label globals p ge pointer_in_fn lbl
-  | None ⇒ return ra
-  ] ;
- let st ≝ set_pc … new_pc st in
- return 〈tr, st〉.
-% qed.
-
-definition eval_call_id:
- ∀globals.∀p:sem_params. genv globals p → state p →
-  ident → call_args p → call_dest p → address → IO io_out io_in (trace×(state p)) ≝
- λglobals,p,ge,st,id,args,dest,ra.
-  ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id) : IO ???;
-  eval_call_block … ge st b args dest ra.
-
-
-(* defining because otherwise typechecker stalls *)
-definition eval_address : ∀globals.∀p : sem_params. genv globals p → state p →
-  ∀i : ident.member i (eq_identifier SymbolTag) globals
-     →dpl_reg p→dph_reg p→ succ p → res (trace × (state p)) ≝
-     λglobals,p,ge,st,ident,prf,ldest,hdest,l.
-     let addr ≝ opt_safe ? (find_symbol ?? ge ident) ? in
-     ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer (block_region addr) addr ? zero_offset) ;
-     ! st ← dpl_store … ldest laddr st;
-     ! st ← dph_store … hdest haddr st;
-     ! st ← next … p l st ;
-     return 〈E0, st〉.
-  [ cases addr //
-  | (* TODO: to prove *)
-    elim daemon
-  ] qed.
-
-(* defining because otherwise typechecker stalls *)
-definition eval_pop : ∀globals.∀p : sem_params. genv globals p → state p →
-  acc_a_reg p → succ p → res (trace × (state p)) ≝
-  λglobals,p,ge,st,dst,l.
-        ! 〈st,v〉 ← pop p st;
-        ! st ← acca_store p p dst v st;
-        ! st ← next p l st ;
-        return 〈E0, st〉.
-
-(* defining because otherwise typechecker stalls *)
-definition eval_sequential :
- ∀globals.∀p:sem_params. genv globals p → state p →
-  joint_instruction p globals → succ p → IO io_out io_in (trace×(state p)) ≝
- λglobals,p,ge,st,seq,l.
+  joint_step p globals →
+  IO io_out io_in ((step_flow p globals)×trace×(state p)) ≝
+ λglobals,p,ge,st,seq.
   match seq with
   [ extension c ⇒
-    ! next_addr ← succ_pc … p l (pc … st) : IO ? ? ? ; 
-    ! 〈next_pc, tr, st〉 ← exec_extended … ge c st next_addr;
-    ! st ← match next_pc with
-      [ None ⇒ next … p l st
-      | Some lbl ⇒ goto … ge lbl st
-      ] ;
-    return 〈tr, st〉
+    exec_extended … ge c st
   | COST_LABEL cl ⇒
-    ! st ← next … p l st ;
-    return 〈Echarge cl, st〉
+    return 〈Proceed ??, Echarge cl, st〉
   | COMMENT c ⇒
-    ! st ← next … p l st ;
-    return 〈E0, st〉 
+    return 〈Proceed ??, E0, st〉
   | LOAD dst addrl addrh ⇒
     ! vaddrh ← dph_arg_retrieve … st addrh ;
@@ -331 +371 @@
     ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
     ! st ← acca_store p … dst v st ;
-    ! st ← next … p l st ;
-    return 〈E0, st〉
+    return 〈Proceed ??, E0, st〉
   | STORE addrl addrh src ⇒
     ! vaddrh ← dph_arg_retrieve … st addrh;
@@ -339 +378 @@
     ! v ← acca_arg_retrieve … st src;
     ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
-    let st ≝ set_m … m' st in
-    ! st ← next … p l st ;
-    return 〈E0, st〉
+    return 〈Proceed ??, E0, set_m … m' st〉
   | COND src ltrue ⇒
     ! v ← acca_retrieve … st src;
     ! b ← bool_of_beval v;
     if b then
-     ! st ← goto … p ge ltrue st ;
-     return 〈E0, st〉
+      return 〈Redirect ?? ltrue, E0, st〉
     else
-     ! st ← next … p l st ;
-     return 〈E0, st〉
+      return 〈Proceed ??, E0, st〉
   | ADDRESS ident prf ldest hdest ⇒
-    eval_address … ge st ident prf ldest hdest l
+    let addr ≝ opt_safe ? (find_symbol ?? ge ident) ? in
+    ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer (block_region addr) addr ? zero_offset) ;
+    ! st' ← dpl_store … ldest laddr st;
+    ! st'' ← dph_store … hdest haddr st';
+    return 〈Proceed ??, E0, st''〉
   | OP1 op dacc_a sacc_a ⇒
     ! v ← acca_retrieve … st sacc_a;
@@ -358 +397 @@
     let v' ≝ BVByte (op1 eval op v) in
     ! st ← acca_store … dacc_a v' st;
-    ! st ← next … l st ;
-    return 〈E0, st〉
+    return 〈Proceed ??, E0, st〉
   | OP2 op dacc_a sacc_a src ⇒
     ! v1 ← acca_arg_retrieve … st sacc_a;
@@ -369 +407 @@
       let v' ≝ BVByte v' in
       let carry ≝ beval_of_bool carry in
-    ! st ← acca_store … dacc_a v' st;
-      let st ≝ set_carry … carry st in
-    ! st ← next … l st ;
-    return 〈E0, st〉
+    ! st' ← acca_store … dacc_a v' st;
+      let st'' ≝ set_carry … carry st' in
+    return 〈Proceed ??, E0, st''〉
   | CLEAR_CARRY ⇒
-    ! st ← next … l (set_carry … BVfalse st) ;
-    return 〈E0, st〉
+    let st' ≝ set_carry … BVfalse st in
+    return 〈Proceed ??, E0, st'〉
   | SET_CARRY ⇒
-    ! st ← next … l (set_carry … BVtrue st) ;
-    return 〈E0, st〉
+    let st' ≝ set_carry … BVtrue st in
+    return 〈Proceed ??, E0, st'〉
   | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
     ! v1 ← acca_arg_retrieve … st sacc_a_reg;
@@ -387 +424 @@
     let v1' ≝ BVByte v1' in
     let v2' ≝ BVByte v2' in
-    ! st ← acca_store … dacc_a_reg v1' st;
-    ! st ← accb_store … dacc_b_reg v2' st;
-    ! st ← next … l st ;
-    return 〈E0, st〉
+    ! st' ← acca_store … dacc_a_reg v1' st;
+    ! st'' ← accb_store … dacc_b_reg v2' st';
+    return 〈Proceed ??, E0, st''〉
   | POP dst ⇒
-    eval_pop … ge st dst l
+    ! 〈st',v〉 ← pop p st;
+    ! st'' ← acca_store p p dst v st';
+    return 〈Proceed ??, E0, st''〉
   | PUSH src ⇒
     ! v ← acca_arg_retrieve … st src;
     ! st ← push … st v;
-    ! st ← next … l st ;
-    return 〈E0, st〉
+    return 〈Proceed ??, E0, st〉
   | MOVE dst_src ⇒
     ! st ← pair_reg_move … st dst_src ;
-    ! st ← next … l st ;
-    return 〈E0, st〉
+    return 〈Proceed ??, E0, st〉
   | CALL_ID id args dest ⇒
-    ! ra ← succ_pc … p l (pc … st) : IO ??? ;
-    eval_call_id … ge st id args dest ra
+    ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id) : IO ???;
+    eval_call_block … ge st b args dest
   ].
+  [ cases addr //
+  | (* TODO: to prove *)
+    elim daemon
+  ] qed.
+
+definition eval_step_flow :
+ ∀globals.∀p:sem_params.step_flow p globals →
+  succ p → stmt_flow p globals ≝
+ λglobals,p,cmd,nxt.
+ match cmd with
+ [ Redirect l ⇒ SRedirect … l
+ | Init id fn args dest ⇒ SInit … id fn args dest nxt
+ | Proceed ⇒ SProceed … nxt
+ ].
 
 definition eval_statement : ∀globals: list ident.∀p:sem_params. genv globals p →
-  state p → IO io_out io_in (trace × (state p)) ≝
- λglobals,p,ge,st.
-  ! s ← fetch_statement … ge st : IO ???; 
-  match s return λ_.IO io_out io_in (trace × (state p)) with
-    [ GOTO l ⇒
-       ! st ← goto … ge l st ;
-       return 〈E0, st〉
-    | RETURN ⇒
+  state p → joint_statement … p globals →
+  IO io_out io_in ((stmt_flow p globals) × trace × (state p)) ≝
+ λglobals,p,ge,st,s.
+  match s with
+    [ GOTO l ⇒ return 〈SRedirect … l, E0, (st : state ?)〉 
+    | RETURN ⇒ return 〈SEnd ??, E0, (st : state ?) 〉
+    | sequential seq l ⇒
+      ! 〈flow, tr, st〉 ← eval_step … ge st seq ;
+      return 〈eval_step_flow … flow l, tr, st〉
+    | extension_fin c ⇒
+      ! 〈flow, tr, st〉 ← exec_fin_extended … ge c st ;
+      return 〈pi1 … flow, tr, st〉
+    ].
+
+definition eval_statement_no_seq : ∀globals: list ident.∀p:sem_params. genv globals p →
+  state p → (Σs : joint_statement … p globals.no_seq … s) →
+  IO io_out io_in ((Σf.flow_no_seq p globals f) × trace × (state p)) ≝
+ λglobals,p,ge,st,s_sig.
+  match s_sig with
+  [ mk_Sig s s_prf ⇒
+    match s return λx.no_seq p globals x → ? with
+    [ GOTO l ⇒ λ_.return 〈«SRedirect … l,?», E0, (st : state ?)〉 
+    | RETURN ⇒ λ_.return 〈«SEnd ??,?», E0, (st : state ?) 〉
+    | sequential seq l ⇒ Ⓧ
+    | extension_fin c ⇒ λ_.exec_fin_extended … ge c st
+    ] s_prf
+  ]. % qed.
+
+let rec rel_io O I A B (P : A → B → Prop) (v1 : IO O I A)
+  (v2 : IO O I B) on v1 : Prop ≝
+  match v1 with
+  [ Value x ⇒
+    match v2 with
+    [ Value y ⇒
+      P x y
+    | _ ⇒ False
+    ]
+  | Wrong _ ⇒
+    match v2 with
+    [ Wrong _ ⇒ True
+    | _ ⇒ False
+    ]
+  | Interact o1 f1 ⇒
+    match v2 with
+    [ Interact o2 f2 ⇒
+      ∃prf:o1 = o2.∀i.rel_io … P (f1 i) (f2 ?)
+    | _ ⇒ False
+    ]
+  ]. <prf @i qed.
+
+definition IORel ≝ λO,I.
+  mk_MonadRel (IOMonad O I) (IOMonad O I)
+    (rel_io O I) ???.
+[//
+|#X #Y #Z #W #relin #relout #m elim m
+  [ #o #f #IH * [#o' #f' | #v | #e] * #EQ destruct(EQ) #G
+    #f1 #f2 #G' whd %{(refl …)} #i
+    @(IH … (G i) f1 f2 G')
+  | #v * [#o #f * | #v' | #e *]
+    #Pvv' #f #g #H normalize @H @Pvv'
+  | #e1 * [#o #f * | #v' *| #e2] * #f #g #_ %
+  ]
+| #X #Y #P #Q #H #m elim m [#o #f #IH | #v | #e] *
+  [1,4,7: #o' #f' [2,3: *]
+    normalize * #prf destruct(prf) normalize #G
+    % [%] normalize #i @IH @G
+  |2,5,8: #v' [1,3: *]
+    @H
+  |*: #e' [1,2: *] //
+  ]
+]
+qed.
+
+lemma IORel_refl : ∀O,I,X,rel.reflexive X rel →
+  reflexive ? (m_rel ?? (IORel O I) ?? rel).
+#O #I #X #rel #H #m elim m
+[ #o #f #IH whd %[%] #i normalize @IH
+| #v @H
+| #e %
+]
+qed.
+
+lemma IORel_transitive : ∀O,I,X,Y,Z,rel1,rel2,rel3.
+  (∀x : X.∀y : Y.∀z : Z.rel1 x y → rel2 y z → rel3 x z) →
+  ∀m,n,o.
+  m_rel ?? (IORel O I) … rel1 m n →
+  m_rel ?? (IORel O I) … rel2 n o →
+  m_rel ?? (IORel O I) … rel3 m o.
+#O #I #X #Y #Z #rel1 #rel2 #rel3 #H #m elim m
+[ #o #f #IH * [#o' #f' * [#o'' #f'' | #v #_ * | #e #_ * ] | #v #x * | #e #x * ]
+  normalize * #EQ #H1 * #EQ' #H2 destruct %[%] normalize #i @(IH ? (f' i)) //
+| #v * [#o #f #x * | #v' * [#o #f #_ * | #v'' |#e #_ *] | #e #x *]
+  @H
+| #e * [#o #f #x * | #v #x * | #e' * [#o #f #_ * | #v #_ * | #e'']] //
+]
+qed.
+
+lemma mr_bind' : ∀M1,M2.∀Rel : MonadRel M1 M2.
+  ∀X,Y,Z,W,relin,relout,m,n.m_rel ?? Rel X Y relin m n →
+  ∀f,g.(∀x,y.relin x y → m_rel ?? Rel Z W relout (f x) (g y)) →
+                  m_rel ?? Rel ?? relout (! x ← m ; f x) (! y ← n ; g y).
+#M1 #M2 #Rel #X #Y #Z #W #relin #relout #m #n #H #f #g #G
+@(mr_bind … H) @G qed.
+
+lemma m_bind_ext_eq' : ∀M : MonadProps.∀X,Y.∀m1,m2 : monad M X.∀f1,f2 : X → monad M Y.
+  m1 = m2 → (∀x.f1 x = f2 x) → ! x ← m1 ; f1 x = ! x ← m2 ; f2 x.
+#M #X #Y #m1 #m2 #f1 #f2 #EQ >EQ @m_bind_ext_eq
+qed.
+
+lemma eval_statement_no_seq_to_normal : ∀globals,p,ge,st,s1,s2.
+  pi1 ?? s1 = s2 →
+  m_rel ?? (IORel ??) ??
+    (λx,y.pi1 ?? (\fst (\fst x)) = \fst (\fst y) ∧
+      \snd (\fst x) = \snd (\fst y) ∧ \snd x = \snd y)
+    (eval_statement_no_seq globals p ge st s1)
+    (eval_statement globals p ge st s2).
+#globals #p #ge #st * * [#s #n | #lbl || #c ]*
+#s2 #EQ destruct(EQ)
+whd in match eval_statement;
+whd in match eval_statement_no_seq;
+normalize nodelta
+[1,2: @(mr_return … (IORel ??)) /3 by pair_destruct, conj/]
+<(m_bind_return … (exec_fin_extended ??????)) in ⊢ (???????%?);
+@(mr_bind … (IORel ??)) [@eq | @IORel_refl // |
+#x #y #EQ destruct(EQ) cases y ** #a #prf #b #c whd /3 by pair_destruct, conj/
+qed.
+
+definition do_call : ∀globals: list ident.∀p:sem_params. genv globals p →
+  state p → Z → joint_internal_function globals p → call_args p →
+  res (state_pc p) ≝
+  λglobals,p,ge,st,id,fn,args.
+    ! st' ← setup_call … (joint_if_stacksize … fn) (joint_if_params … fn)
+              args st ;
+    let regs ≝ foldr ?? (allocate_local p p) (regs … st) (joint_if_locals … fn) in
+    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 pc ≝ pointer_of_point ? p … pointer_in_fn l' in
+    return mk_state_pc ? st' pc. % qed.
+
+definition eval_stmt_flow : ∀globals: list ident.∀p:sem_params. genv globals p →
+  state_pc p → stmt_flow p globals → IO io_out io_in (state_pc p) ≝
+  λglobals,p,ge,st,flow.
+  match flow with
+  [ SRedirect l ⇒ goto … ge l st
+  | SProceed nxt ⇒ next ? nxt st
+  | SInit id fn args dest nxt ⇒
+    ! ra ← succ_pc ? p … (pc … st) nxt ;
+    let st' ≝ set_no_pc … (set_frms … (save_frame … ra dest st) st) st in
+    do_call ?? ge st' id fn args
+  | STailInit id fn args ⇒
+    do_call … ge st id fn args
+  | SEnd ⇒
+    ! 〈st,ra〉 ← fetch_ra … st ;
+    ! st' ← pop_frame … ge st;
+    return mk_state_pc ? st' ra
+  ].
+
+definition eval_stmt_flow_no_seq : ∀globals: list ident.∀p:sem_params. genv globals p →
+  state p → Z → (Σf:stmt_flow p globals.flow_no_seq … f) →
+    IO io_out io_in (state_pc p) ≝
+  λglobals,p,ge,st,id,flow_sig.
+  match flow_sig with
+  [ mk_Sig flow prf ⇒
+    match flow return λx.flow_no_seq p globals x → ? with
+    [ SRedirect l ⇒ λ_.
+      ! newpc ← pointer_of_label ? p … ge
+        (mk_pointer Code (mk_block Code id) ? (mk_offset 0)) l ;
+      return mk_state_pc … st newpc
+    | STailInit id fn args ⇒ λ_.
+      do_call … ge st id fn args
+    | SEnd ⇒ λ_.
       ! 〈st,ra〉 ← fetch_ra … st ;
-      ! st ← pop_frame … ge st;
-      return 〈E0,set_pc … ra st〉
-   | sequential seq l ⇒ eval_sequential … ge st seq l
-   | extension_fin c ⇒ exec_fin_extended … ge c st
-   ].
+      ! st' ← pop_frame … ge st;
+      return mk_state_pc ? st' ra
+    | _ ⇒ Ⓧ
+    ] prf
+  ]. % qed.
+
+lemma pointer_of_label_eq_with_id :
+∀g.∀p : sem_params.∀ge : genv g p.∀ptr1,ptr2 : cpointer.∀lbl.
+  block_id (pblock ptr1) = block_id (pblock ptr2) →
+  pointer_of_label ? p ? ge ptr1 lbl = pointer_of_label ? p ? ge ptr2 lbl.
+#g #p #ge
+** #ty1 * #r1 #id1 #H1 inversion H1 [#s || #s] #id #EQ1 #EQ2 #EQ3 #o #EQ4 destruct
+** #ty2 * #r2 #id2 #H2 inversion H2
+[1,3: #s] #id2' #EQ5 #EQ6 #EQ7 #o2 #EQ8 #lbl #EQ9 destruct %
+qed.
+
+
+lemma eval_stmt_flow_no_seq_to_normal : ∀g.∀p : sem_params.∀ge.∀st : state_pc p.
+  ∀id.∀s1 : Σs.flow_no_seq p g s.∀s2.
+  pi1 … s1 = s2 → block_id (pblock (pc … st)) = id →
+    (eval_stmt_flow_no_seq g p ge st id s1) =
+    (eval_stmt_flow g p ge st s2).
+#g#p#ge#st#id'
+**[#lbl|#nxt*|#id#fn#args#dest#n*|#id#fn#args]*
+#s2 #EQ #EQ' destruct(EQ)
+whd in match eval_stmt_flow_no_seq; normalize nodelta
+whd in match eval_stmt_flow; normalize nodelta
+[2,3: %]
+whd in match goto; normalize nodelta
+whd in match set_pc; normalize nodelta
+>pointer_of_label_eq_with_id [% | >EQ' % |]
+qed.
+
+definition eval_state : ∀globals: list ident.∀p:sem_params. genv globals p →
+  state_pc p → IO io_out io_in (trace × (state_pc p)) ≝
+  λglobals,p,ge,st.
+  ! s ← fetch_statement ? p … ge (pc … st) : IO ???;
+  ! 〈flow, tr, st_npc〉 ← eval_statement … ge st s;
+  let st ≝ set_no_pc … st_npc st in
+  ! st ← eval_stmt_flow … ge st flow;
+  return 〈tr, st〉.
 
 definition is_final: ∀globals:list ident. ∀p: sem_params.
-  genv globals p → address → state p → option int ≝
+  genv globals p → cpointer → state_pc p → option int ≝
  λglobals,p,ge,exit,st.res_to_opt ? (
-  do s ← fetch_statement … ge st;
+  do s ← fetch_statement ? p … ge (pc … st);
   match s with
    [ RETURN ⇒ 
       do 〈st,ra〉 ← fetch_ra … st; 
-      if eq_address ra exit then 
+      if eq_pointer ra exit then 
        do vals ← read_result … ge st ;
        Word_of_list_beval vals
@@ -436 +686 @@
        Error ? [ ]
    | _ ⇒ Error ? [ ]]).
-
+ 
 record evaluation_parameters : Type[1] ≝
  { globals: list ident
  ; sparams:> sem_params
- ; exit: address
+ ; exit: cpointer
  ; genv2: genv globals sparams
  }.
 
 definition joint_exec: trans_system io_out io_in ≝
-  mk_trans_system … evaluation_parameters (λG. state G)
+  mk_trans_system … evaluation_parameters (λG. state_pc G)
    (λG.is_final (globals G) G (genv2 G) (exit G))
-   (λG.eval_statement (globals G) G (genv2 G)).
+   (λG.eval_state (globals G) G (genv2 G)).
 
 definition make_global :
@@ -457 +707 @@
  let b ≝ mk_block Code (-1) in
  let ptr ≝ mk_pointer Code b ? (mk_offset 0) in
- let addr ≝ address_of_code_pointer ptr in
   (λp. mk_evaluation_parameters
     (prog_var_names … p)
     (mk_sem_params … pars)
-    addr
+    ptr
     (globalenv Genv … p)
   ).
@@ -470 +719 @@
 definition make_initial_state :
  ∀pars: sem_params.
- ∀p: joint_program … pars. res (state pars) ≝
+ ∀p: joint_program … pars. res (state_pc pars) ≝
 λpars,p.
   let sem_globals ≝ make_global pars p in
@@ -480 +729 @@
   let spp ≝ mk_pointer XData spb ? (mk_offset external_ram_size) in
   let ispp ≝ mk_pointer XData ispb ? (mk_offset 47) in
-  do sp ← address_of_pointer spp ;
   let main ≝ prog_main … p in
-  let st0 ≝ mk_state … (empty_framesT …) sp ispp dummy_pc BVfalse (empty_regsT … sp) m in
-  let trace_state ≝
-   eval_call_id … pars ge st0 main (call_args_for_main … pars)
-    (call_dest_for_main … pars) (exit sem_globals) in
-  match trace_state with
-  [ Value tr_st ⇒ OK … (\snd tr_st) (* E0 trace thrown away *)
-  | Wrong msg ⇒ Error … msg
-  | Interact _ _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
-  ].
-[3: % | cases ispb | cases spb] * #r #off #E >E %
+  let st0 ≝ mk_state pars (empty_framesT …) spp ispp BVfalse (empty_regsT … spp) m in
+  (* use exit sem_globals as ra and call_dest_for_main as dest *)
+  let st0' ≝ set_frms ? (save_frame … (exit sem_globals) (call_dest_for_main … pars) st0) st0 in
+  let st_pc0 ≝ mk_state_pc ? st0' dummy_pc in
+  ! main_block ← opt_to_res … [MSG MissingSymbol; CTX ? main] (find_symbol ?? ge main) ;
+  ! main_fd ← opt_to_res ? [MSG BadPointer] (find_funct_ptr ?? ge main_block) ; 
+  match main_fd with
+  [ Internal fn ⇒
+    do_call ?? ge st_pc0 (block_id main_block) fn (call_args_for_main … pars)
+  | External _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
+  ]. [5: cases ispb * |6: cases spb * ] (* without try it fails! *) try //
 qed.