Changeset 1882 for src/joint/Joint_paolo.ma

Timestamp:

Apr 6, 2012, 8:02:10 PM (9 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

File:

• src/joint/Joint_paolo.ma (modified) (11 diffs)

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 ≝