Changeset 2252 for src/Cminor

Timestamp:

Jul 24, 2012, 7:40:21 PM (8 years ago)

Author:

campbell

Message:

Use the return statement invariant. Restructure the invariants for Cminor
a bit to make them more understandable.

Location:

src/Cminor

Files:

• initialisation.ma (modified) (3 diffs)
• syntax.ma (modified) (2 diffs)
• toRTLabs.ma (modified) (32 diffs)

src/Cminor/initialisation.ma

@@ -38 +38 @@
     ]
 ].
-% /2/
+% /3/
 cases init in p; [ 7: | 8: #a #b | *: #a ] #p normalize in p;
-destruct;/3/
+destruct;/4 by stmt_labels_mp, conj/
 qed.
 
@@ -50 +50 @@
      〈off + (size_init_data datum), St_seq (init_datum id r datum off) s〉)
   〈0, mk_Sig ? (λx.stmt_inv x) St_skip ?〉 init).
-[ % /2/
+[ % /3/
 | elim init
-  [ % /2/
-  | #h #t #IH whd in ⊢ (?(???%)); @breakup_pair whd in ⊢ (?%);
-    % [ % [ % /2/ | @(pi2 … (init_datum …)) ] | @IH ]
+  [ % /3/
+  | #h #t #IH whd in ⊢ (?(???%)); @breakup_pair
+    %
+    [ /3/
+    | % [ @(pi2 … (init_datum …)) | @IH ]
+    ]
 ] qed. 
 
 definition init_vars : list (ident × region × (list init_data)) → Σs:stmt. stmt_inv s ≝
 λvars. foldr ? (Σs:stmt. stmt_inv s)
-  (λvar,s. mk_Sig ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst var)) (\snd (\fst var)) (\snd var))) ?) (mk_Sig ? (λx.stmt_inv x ) St_skip (conj ?? (conj ?? I I) I)) vars.
-% [ % [ % /2/ | @(pi2 … s) ] | @(pi2 … (init_var …)) ]
-qed.
+  (λvar,s. mk_Sig ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst var)) (\snd (\fst var)) (\snd var))) ?) (mk_Sig ? (λx.stmt_inv x ) St_skip ?) vars.
+[ % [ /3/ | % [ @(pi2 … s) | @(pi2 … (init_var …)) ] ]
+| /4/
+] qed.
 
 lemma no_labels : ∀s. stmt_inv s → labels_of s = [ ].
 #s elim s //
-[ #s1 #s2 #IH1 #IH2 * * * * #_ #_ #_ #H1 #H2 whd in ⊢ (??%?);
+[ #s1 #s2 #IH1 #IH2 * #_ * #H1 #H2 whd in ⊢ (??%?);
   >(IH1 H1) >(IH2 H2) @refl 
-| #sz #sg #e #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?);
+| #sz #sg #e #s1 #s2 #IH1 #IH2 * #_ * #H1 #H2 whd in ⊢ (??%?);
   >(IH1 H1) >(IH2 H2) @refl
 | #l #s #IH * * * #_ *
-| #l #s #IH * * #_ #_ #H @(IH H)
+| #l #s #IH * #_ #H @(IH H)
 ] qed.
 
@@ -95 +99 @@
       | inr _ ⇒ 〈id',f'〉 ]) ].
 %
-[ % [ % // |
-  @(stmt_P_mp … H) #s * * #V #L #R %
-  [ @(stmt_vars_mp … V) #i #t *
-  | @(stmt_labels_mp … L) #l *
-  | cases s in R ⊢ %; // #x *
+[ % //
+| %
+  [ @(stmt_P_mp … H) #s * * #V #L #R %
+    [ @(stmt_vars_mp … V) #i #t *
+    | @(stmt_labels_mp … L) #l *
+    | cases s in R ⊢ %; // #x *
+    ]
+  | whd in match (labels_of ?); >(no_labels … H) @(f_inv f)
   ]
-  ]
-| whd in match (labels_of ?); >(no_labels … H) @(f_inv f)
 ] qed.
 

src/Cminor/syntax.ma

@@ -51 +51 @@
 | St_cost : costlabel → stmt → stmt.
 
+(* Apply a predicate to every statement.  Be careful with grouping so that the
+   local application is the first conjunct, and substatements the second. *)
+
 let rec stmt_P (P:stmt → Prop) (s:stmt) on s : Prop ≝
 match s with
-[ St_seq s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2
-| St_ifthenelse _ _ _ s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2
+[ St_seq s1 s2 ⇒ P s ∧ (stmt_P P s1 ∧ stmt_P P s2)
+| St_ifthenelse _ _ _ s1 s2 ⇒ P s ∧ (stmt_P P s1 ∧ stmt_P P s2)
 | St_label _ s' ⇒ P s ∧ stmt_P P s'
 | St_cost _ s' ⇒ P s ∧ stmt_P P s'
-| _ ⇒ P s
+| _ ⇒ P s ∧ True
 ].
 
 lemma stmt_P_P : ∀P,s. stmt_P P s → P s.
-#P * normalize /2/
-[ #s1 #s2 * * /2/
-| #sz #sg #e #s1 #s2 * * /2/ 
-| *: #i #s normalize * /2/
-] qed.
+#P * normalize * /3 by proj1/
+qed.
 
 (* Assert a predicate on every variable or parameter identifier. *)
@@ -91 +91 @@
 
 lemma stmt_P_mp : ∀P,Q. (∀s. P s → Q s) → ∀s. stmt_P P s → stmt_P Q s.
-#P #Q #H #s elim s /2/
-[ #s1 #s2 #H1 #H2 normalize * * /4/
-| #sz #sg #e #s1 #s2 #H1 #H2 * * /5/
-| #l #s #H * /5/
-| #l #s #H * /5/
-] qed.
+#P #Q #H #s elim s /6 by proj1, proj2, conj/
+qed.
 
 lemma stmt_vars_mp : ∀P,Q. (∀i,t. P i t → Q i t) → ∀s. stmt_vars P s → stmt_vars Q s.

src/Cminor/toRTLabs.ma

@@ -192 +192 @@
  λe,g. forall_nodes ? (labels_P (λl. present ?? g l ∨ lpresent e l)) g.
 
+(* Some data structures for the transformation that remain fixed throughout. *)
+record fixed : Type[0] ≝ {
+  fx_lenv   : label_env;
+  fx_env    : env;
+  fx_rettyp : option typ
+}.
+
+definition resultok : option typ → list (register × typ) → Type[0] ≝ 
+λty,env.
+  match ty with [ Some t ⇒ Σr:register. env_has env r t | _ ⇒ True ].
+
 (* I'd use a single parametrised definition along with internal_function, but
    it's a pain without implicit parameters. *)
-record partial_fn (lenv:label_env) (env:env) : Type[0] ≝
+record partial_fn (fx:fixed) : Type[0] ≝
 { pf_labgen    : universe LabelTag
 ; pf_reggen    : universe RegisterTag
 ; pf_params    : list (register × typ)
 ; pf_locals    : list (register × typ)
-; pf_result    : option (Σrt:register × typ. env_has (pf_locals @ pf_params) (\fst rt) (\snd rt))
-; pf_envok     : ∀id,ty,r,H. lookup_reg env id ty H = r → env_has (pf_locals @ pf_params) r ty
+; pf_result    : resultok (fx_rettyp … fx) (pf_locals @ pf_params)
+; pf_envok     : ∀id,ty,r,H. lookup_reg (fx_env … fx) id ty H = r → env_has (pf_locals @ pf_params) r ty
 ; pf_stacksize : nat
 ; pf_graph     : graph statement
-; pf_closed    : partially_closed lenv pf_graph
+; pf_closed    : partially_closed (fx_lenv … fx) pf_graph
 ; pf_typed     : graph_typed (pf_locals @ pf_params) pf_graph
 ; pf_entry     : Σl:label. present ?? pf_graph l
@@ -210 +221 @@
 
 definition fn_env_has ≝
-  λle,env,f. env_has (pf_locals le env f @ pf_params le env f).
-
-record fn_contains (le:label_env) (env:env) (f1:partial_fn le env) (f2:partial_fn le env) : Prop ≝
+  λfx,f. env_has (pf_locals fx f @ pf_params fx f).
+
+record fn_contains (fx:fixed) (f1:partial_fn fx) (f2:partial_fn fx) : Prop ≝
 { fn_con_graph : graph_included (pf_graph … f1) (pf_graph … f2)
-; fn_con_env : ∀r,ty. fn_env_has le env f1 r ty → fn_env_has le env f2 r ty
+; fn_con_env : ∀r,ty. fn_env_has … f1 r ty → fn_env_has … f2 r ty
 }.
 
-lemma fn_con_trans : ∀le,env,f1,f2,f3.
-  fn_contains le env f1 f2 → fn_contains le env f2 f3 → fn_contains le env f1 f3.
-#le #env #f1 #f2 #f3 #H1 #H2 %
+lemma fn_con_trans : ∀fx,f1,f2,f3.
+  fn_contains fx f1 f2 → fn_contains … f2 f3 → fn_contains … f1 f3.
+#fx #f1 #f2 #f3 #H1 #H2 %
 [ @(graph_inc_trans … (fn_con_graph … H1) (fn_con_graph … H2))
 | #r #ty #H @(fn_con_env … H2) @(fn_con_env … H1) @H
 ] qed.
 
-lemma fn_con_refl : ∀label_env,env,f.
-  fn_contains label_env env f f.
-#le #env #f % #l // qed.
-
-lemma fn_con_sig : ∀label_env,env,f,f0.
-  ∀f':Σf':partial_fn label_env env. fn_contains … f0 f'.
-  fn_contains label_env env f f0 →
-  fn_contains label_env env f f'.
-#le #env #f #f0 * #f' #H1 #H2 @(fn_con_trans … H2 H1)
-qed.
-
-lemma add_statement_inv : ∀le,env,l,s.∀f.
-  labels_present (pf_graph le env f) s →
-  partially_closed le (add … (pf_graph … f) l s).
-#le #env #l #s #f #p
+lemma fn_con_refl : ∀fx,f.
+  fn_contains fx f f.
+#fx #f % #l // qed.
+
+lemma fn_con_sig : ∀fx,f,f0.
+  ∀f':Σf':partial_fn fx. fn_contains … f0 f'.
+  fn_contains fx f f0 →
+  fn_contains fx f f'.
+#fx #f #f0 * #f' #H1 #H2 @(fn_con_trans … H2 H1)
+qed.
+
+lemma add_statement_inv : ∀fx,l,s.∀f.
+  labels_present (pf_graph fx f) s →
+  partially_closed (fx_lenv … fx) (add … (pf_graph … f) l s).
+#fx #l #s #f #p
 #l' #s' #H cases (identifier_eq … l l')
 [ #E >E in H; >lookup_add_hit #E' <(?:s = s') [2:destruct //]
@@ -249 +260 @@
 
 definition statement_typed_in ≝
-λle,env,f,s. statement_typed (pf_locals le env f @ pf_params le env f) s.
+λfx,f,s. statement_typed (pf_locals fx f @ pf_params fx f) s.
 
 lemma forall_nodes_add : ∀A,P,l,a,g.
@@ -261 +272 @@
 
 (* Add a statement to the graph, *without* updating the entry label. *)
-definition fill_in_statement : ∀le,env. label → ∀s:statement. ∀f:partial_fn le env.
+definition fill_in_statement : ∀fx. label → ∀s:statement. ∀f:partial_fn fx.
   labels_present (pf_graph … f) s →
-  statement_typed_in le env f s →
-  Σf':partial_fn le env. fn_contains … f f' ≝
-λle,env,l,s,f,p,tp.
-  mk_partial_fn le env (pf_labgen … f) (pf_reggen … f)
+  statement_typed_in … f s →
+  Σf':partial_fn fx. fn_contains … f f' ≝
+λfx,l,s,f,p,tp.
+  mk_partial_fn fx (pf_labgen … f) (pf_reggen … f)
                 (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
                 (pf_stacksize … f) (add ?? (pf_graph … f) l s) ? ?
@@ -277 +288 @@
 
 (* Add a statement to the graph, making it the entry label. *)
-definition add_to_graph : ∀le,env. label → ∀s:statement. ∀f:partial_fn le env.
+definition add_to_graph : ∀fx. label → ∀s:statement. ∀f:partial_fn fx.
   labels_present (pf_graph … f) s →
   statement_typed_in … f s →
-  Σf':partial_fn le env. fn_contains … f f' ≝
-λle,env,l,s,f,p,tl.
-  mk_partial_fn le env (pf_labgen … f) (pf_reggen … f)
+  Σf':partial_fn fx. fn_contains … f f' ≝
+λfx,l,s,f,p,tl.
+  mk_partial_fn fx (pf_labgen … f) (pf_reggen … f)
                 (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
                 (pf_stacksize … f) (add ?? (pf_graph … f) l s) ? ?
@@ -295 +306 @@
 (* Add a statement with a fresh label to the start of the function.  The
    statement is parametrised by the *next* instruction's label. *)
-definition add_fresh_to_graph : ∀le,env. ∀s:(label → statement). ∀f:partial_fn le env.
+definition add_fresh_to_graph : ∀fx. ∀s:(label → statement). ∀f:partial_fn fx.
   (∀l. present ?? (pf_graph … f) l → labels_present (pf_graph … f) (s l)) →
   (∀l. statement_typed_in … f (s l)) →
-  Σf':partial_fn le env. fn_contains … f f' ≝
-λle,env,s,f,p,tp.
+  Σf':partial_fn fx. fn_contains … f f' ≝
+λfx,s,f,p,tp.
   let 〈l,g〉 ≝ fresh … (pf_labgen … f) in
   let s' ≝ s (pf_entry … f) in
-    (mk_partial_fn le env g (pf_reggen … f)
+    (mk_partial_fn fx g (pf_reggen … f)
                    (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
                    (pf_stacksize … f) (add ?? (pf_graph … f) l s') ? ?
@@ -315 +326 @@
 (* Variants for labels which are (goto) labels *)
 
-lemma add_statement_inv' : ∀le,env,l,s.∀f.
-  labels_P (λl. present ?? (pf_graph le env f) l ∨ lpresent le l) s →
-  partially_closed le (add … (pf_graph … f) l s).
-#le #env #l #s #f #p
+lemma add_statement_inv' : ∀fx,l,s.∀f.
+  labels_P (λl. present ?? (pf_graph fx f) l ∨ lpresent (fx_lenv … fx) l) s →
+  partially_closed (fx_lenv … fx) (add … (pf_graph … f) l s).
+#fx #l #s #f #p
 #l' #s' #H cases (identifier_eq … l l')
 [ #E >E in H; >lookup_add_hit #E' <(?:s = s') [2:destruct //]
@@ -328 +339 @@
 ] qed.
 
-definition add_fresh_to_graph' : ∀le,env. ∀s:(label → statement). ∀f:partial_fn le env. 
-  (∀l. present ?? (pf_graph … f) l → labels_P (λl.present ?? (pf_graph … f) l ∨ lpresent le l) (s l)) →
+definition add_fresh_to_graph' : ∀fx. ∀s:(label → statement). ∀f:partial_fn fx. 
+  (∀l. present ?? (pf_graph … f) l → labels_P (λl.present ?? (pf_graph … f) l ∨ lpresent (fx_lenv … fx) l) (s l)) →
   (∀l. statement_typed_in … f (s l)) →
-  Σf':partial_fn le env. fn_contains … f f' ≝
-λle,env,s,f,p,tp.
+  Σf':partial_fn fx. fn_contains … f f' ≝
+λfx,s,f,p,tp.
   let 〈l,g〉 ≝ fresh … (pf_labgen … f) in
   let s' ≝ s (pf_entry … f) in
-    (mk_partial_fn le env g (pf_reggen … f)
+    (mk_partial_fn fx g (pf_reggen … f)
                    (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
                    (pf_stacksize … f) (add ?? (pf_graph … f) l s') ? ?
@@ -362 +373 @@
 (* A little more nesting in the result type than I'd like, but it keeps the 
    function closely paired with the proof that it contains f. *)
-definition fresh_reg : ∀le,env. ∀f:partial_fn le env. ∀ty:typ.
-  𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σr:register. fn_env_has le env f' r ty) ≝
-λle,env,f,ty.
+definition fresh_reg : ∀fx. ∀f:partial_fn fx. ∀ty:typ.
+  𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σr:register. fn_env_has … f' r ty) ≝
+λfx,f,ty.
   let 〈r,g〉 ≝ fresh … (pf_reggen … f) in
   let f' ≝
-    «mk_partial_fn le env
-       (pf_labgen … f) g (pf_params … f) (〈r,ty〉::(pf_locals … f))
-       (match pf_result … f with [ None ⇒ None ? | Some rt ⇒ Some ? «pi1 … rt, ?»]) ?
+    «mk_partial_fn fx
+       (pf_labgen … f) g (pf_params … f) (〈r,ty〉::(pf_locals … f)) ? ?
        (pf_stacksize … f) (pf_graph … f) (pf_closed … f) ? (pf_entry … f) (pf_exit … f), ?»
   in
@@ -376 +386 @@
 | #l #s #L @stmt_extend_typ_env @(pf_typed … L)
 | #i #t #r1 #H #L %2 @(pf_envok … f … L)
-| %2 @(pi2 … rt)
+| lapply (pf_result fx f) cases (fx_rettyp fx) // #t * #r' #H %{r'} @extend_typ_env //
 | % [ #l // | #r' #ty' #H @extend_typ_env @H ]
 ] qed.
@@ -382 +392 @@
 axiom UnknownVariable : String.
 
-definition choose_reg : ∀le. ∀env:env.∀ty.∀e:expr ty. ∀f:partial_fn le env. expr_vars ty e (Env_has env) →
-  𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σr:register. fn_env_has le env f' r ty) ≝
-λle,env,ty,e,f.
-  match e return λty,e. expr_vars ty e (Env_has env) → 𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σr:register. fn_env_has le env f' r ty) with
-  [ Id t i ⇒ λEnv. ❬«f, ?», «lookup_reg env i t Env, ?»❭
-  | _ ⇒ λ_.fresh_reg le env f ?
+definition choose_reg : ∀fx.∀ty.∀e:expr ty. ∀f:partial_fn fx. expr_vars ty e (Env_has (fx_env fx)) →
+  𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σr:register. fn_env_has … f' r ty) ≝
+λfx,ty,e,f.
+  match e return λty,e. expr_vars ty e (Env_has (fx_env fx)) → 𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σr:register. fn_env_has … f' r ty) with
+  [ Id t i ⇒ λEnv. ❬«f, ?», «lookup_reg (fx_env fx) i t Env, ?»❭
+  | _ ⇒ λ_.fresh_reg … f ?
   ].
 [ % //
@@ -404 +414 @@
 λA,P,x. match x with [ mk_DPair a _ ⇒ a].
 
-definition choose_regs : ∀le. ∀env:env. ∀es:list (𝚺t:typ.expr t).
-                         ∀f:partial_fn le env. All ? (exprtyp_present env) es →
-                         𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has le env f' r (eject' typ expr e)) rs es) ≝
-λle,env,es,f,Env.
-  foldr_all' (𝚺t:typ.expr t) ? (λes. 𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has le env f' r (eject' typ expr e)) rs es))
+definition choose_regs : ∀fx. ∀es:list (𝚺t:typ.expr t).
+                         ∀f:partial_fn fx. All ? (exprtyp_present (fx_env fx)) es →
+                         𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has … f' r (eject' typ expr e)) rs es) ≝
+λfx,es,f,Env.
+  foldr_all' (𝚺t:typ.expr t) ? (λes. 𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has … f' r (eject' typ expr e)) rs es))
     (λe,p,tl,acc.
-      match acc return λ_.𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has le env f' r (eject' typ expr e)) rs (e::tl)) with [ mk_DPair f1 rs ⇒
-        match e return λe.exprtyp_present env e → 𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has le env f' r (eject' typ expr e)) rs (e::tl)) with [ mk_DPair t e ⇒ λp.
-          match choose_reg le env t e (pi1 … f1) ? return λ_.𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has le env f' r (eject' typ expr e)) rs (❬t,e❭::tl)) with [ mk_DPair f' r ⇒
+      match acc return λ_.𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has … f' r (eject' typ expr e)) rs (e::tl)) with [ mk_DPair f1 rs ⇒
+        match e return λe.exprtyp_present (fx_env fx) e → 𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has … f' r (eject' typ expr e)) rs (e::tl)) with [ mk_DPair t e ⇒ λp.
+          match choose_reg fx t e (pi1 … f1) ? return λ_.𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has … f' r (eject' typ expr e)) rs (❬t,e❭::tl)) with [ mk_DPair f' r ⇒
             ❬«pi1 … f', ?»,«(pi1 … r)::(pi1 … rs), ?»❭
           ]
@@ -419 +429 @@
 [ @p
 | cases r #r' #Hr' cases rs #rs' #Hrs'
-  % [ whd in ⊢ (???%%%); @Hr' | @(All2_mp … Hrs') #r1 * #t1 #e1 #H1 @(fn_con_env … f1) [ @(pi2 … f') | @H1 ] ]
+  % [ whd in ⊢ (??%%%); @Hr' | @(All2_mp … Hrs') #r1 * #t1 #e1 #H1 @(fn_con_env … f1) [ @(pi2 … f') | @H1 ] ]
 | @fn_con_trans [ 3: @(pi2 … f') | skip | @(pi2 … f1) ]
 | @fn_con_refl
@@ -430 +440 @@
 
 
-lemma choose_regs_length : ∀le,env,es,f,p,f',rs.
-  choose_regs le env es f p = ❬f',rs❭ → |es| = length … rs.
-#le #env #es #f #p #f' * #rs #H #_ @sym_eq @(All2_length … H)
-qed.
-
-lemma present_included : ∀le,env,f,f',l.
-  fn_contains le env f f' →
+lemma choose_regs_length : ∀fx,es,f,p,f',rs.
+  choose_regs fx es f p = ❬f',rs❭ → |es| = length … rs.
+#fx #es #f #p #f' * #rs #H #_ @sym_eq @(All2_length … H)
+qed.
+
+lemma present_included : ∀fx,f,f',l.
+  fn_contains fx f f' →
   present ?? (pf_graph … f) l →
   present ?? (pf_graph … f') l.
-#le #env #f #f' #l * #H1 #H2 @H1 qed.
+#fx #f #f' #l * #H1 #H2 @H1 qed.
 
 (* Some definitions for the add_stmt function later, which we introduce now so
@@ -446 +456 @@
 (* We need to show that the graph only grows, and that Cminor labels will end
    up in the graph. *)
-definition Cminor_labels_added ≝ λle,env,s,f'.
+definition Cminor_labels_added ≝ λfx,s,f'.
 ∀l. Exists ? (λl'.l=l') (labels_of s) →
-∃l'. lookup ?? le l = Some ? l' ∧ present ?? (pf_graph le env f') l'.
-
-record add_stmt_inv (le:label_env) (env:env) (s:stmt) (f:partial_fn le env) (f':partial_fn le env) : Prop ≝
+∃l'. lookup ?? (fx_lenv fx) l = Some ? l' ∧ present ?? (pf_graph fx f') l'.
+
+record add_stmt_inv (fx:fixed) (s:stmt) (f:partial_fn fx) (f':partial_fn fx) : Prop ≝
 { stmt_graph_con : fn_contains … f f'
 ; stmt_labels_added : Cminor_labels_added … s f'
@@ -458 +468 @@
 
 (* A datatype saying how we intend to prove a step. *)
-inductive fn_con_because (le:label_env) (env:env) : partial_fn le env → Type[0] ≝
-| fn_con_eq : ∀f. fn_con_because le env f
-| fn_con_sig : ∀f1,f2:partial_fn le env. fn_contains … f1 f2 →
-    ∀f3:(Σf3:partial_fn le env.fn_contains … f2 f3). fn_con_because le env f3
-| fn_con_addinv : ∀f1,f2:partial_fn le env. fn_contains … f1 f2 →
-    ∀s.∀f3:(Σf3:partial_fn le env.add_stmt_inv … s f2 f3). fn_con_because le env f3
+inductive fn_con_because (fx:fixed) : partial_fn fx → Type[0] ≝
+| fn_con_eq : ∀f. fn_con_because fx f
+| fn_con_sig : ∀f1,f2:partial_fn fx. fn_contains … f1 f2 →
+    ∀f3:(Σf3:partial_fn fx.fn_contains … f2 f3). fn_con_because fx f3
+| fn_con_addinv : ∀f1,f2:partial_fn fx. fn_contains … f1 f2 →
+    ∀s.∀f3:(Σf3:partial_fn fx.add_stmt_inv … s f2 f3). fn_con_because fx f3
 .
 
 (* Extract the starting function for a step. *)
-let rec fn_con_because_left le env f0  (b:fn_con_because ?? f0) on b : partial_fn le env ≝
+let rec fn_con_because_left fx f0  (b:fn_con_because ? f0) on b : partial_fn fx ≝
   match b with [ fn_con_eq f ⇒ f | fn_con_sig f _ _ _ ⇒ f | fn_con_addinv f _ _ _ _ ⇒ f ].
 
@@ -475 +485 @@
    have reached the desired starting point. *)
 
-unification hint 0 ≔ le:label_env, env:env, f:partial_fn le env, dummy:True;
+unification hint 0 ≔ fx:fixed, f:partial_fn fx, dummy:True;
   f' ≟ f,
-  b  ≟ fn_con_eq le env f
+  b  ≟ fn_con_eq fx f
 ⊢
-  fn_contains le env f f' ≡ fn_contains le env (fn_con_because_left le env f' b) f'
+  fn_contains fx f f' ≡ fn_contains fx (fn_con_because_left fx f' b) f'
 .
 
-unification hint 1 ≔ le:label_env, env:env, f1:partial_fn le env, f2:partial_fn le env, H12 : fn_contains le env f1 f2, f3:(Σf3:partial_fn le env. fn_contains le env f2 f3);
-  b ≟ fn_con_sig le env f1 f2 H12 f3
+unification hint 1 ≔ fx:fixed, f1:partial_fn fx, f2:partial_fn fx, H12 : fn_contains fx f1 f2, f3:(Σf3:partial_fn fx. fn_contains fx f2 f3);
+  b ≟ fn_con_sig fx f1 f2 H12 f3
 ⊢
-  fn_contains le env f1 f3 ≡ fn_contains le env (fn_con_because_left le env f3 b) f3
+  fn_contains fx f1 f3 ≡ fn_contains fx (fn_con_because_left fx f3 b) f3
 .
 
-unification hint 1 ≔ le:label_env, env:env, f1:partial_fn le env, f2:partial_fn le env, H12 : fn_contains le env f1 f2, s:stmt, f3:(Σf3:partial_fn le env. add_stmt_inv le env s f2 f3);
-  b ≟ fn_con_addinv le env f1 f2 H12 s f3
+unification hint 1 ≔ fx:fixed, f1:partial_fn fx, f2:partial_fn fx, H12 : fn_contains fx f1 f2, s:stmt, f3:(Σf3:partial_fn fx. add_stmt_inv fx s f2 f3);
+  b ≟ fn_con_addinv fx f1 f2 H12 s f3
 ⊢
-  fn_contains le env f1 f3 ≡ fn_contains le env (fn_con_because_left le env f3 b) f3
+  fn_contains fx f1 f3 ≡ fn_contains fx (fn_con_because_left fx f3 b) f3
 .
 
 (* A lemma to perform a step of the proof.  We can repeat this to do the whole
    proof. *)  
-lemma fn_contains_step : ∀le,env,f. ∀b:fn_con_because le env f. fn_contains … (fn_con_because_left … f b) f.
-#le #env #f *
+lemma fn_contains_step : ∀fx,f. ∀b:fn_con_because fx f. fn_contains … (fn_con_because_left … f b) f.
+#fx #f *
 [ #f @fn_con_refl
 | #f1 #f2 #H12 * #f3 #H23 @(fn_con_trans … H12 H23)
@@ -505 +515 @@
 axiom BadCminorProgram : String.
 
-let rec add_expr (le:label_env) (env:env) (ty:typ) (e:expr ty)
-  (Env:expr_vars ty e (Env_has env)) (f:partial_fn le env)
+let rec add_expr (fx:fixed) (ty:typ) (e:expr ty)
+  (Env:expr_vars ty e (Env_has (fx_env fx))) (f:partial_fn fx)
   (dst:Σdst. fn_env_has … f dst ty)
-  on e: Σf':partial_fn le env. fn_contains … f f' ≝
-match e return λty,e.expr_vars ty e (Env_has env) → (Σdst. fn_env_has … f dst ty) → Σf':partial_fn le env. fn_contains … f f' with
+  on e: Σf':partial_fn fx. fn_contains … f f' ≝
+match e return λty,e.expr_vars ty e (Env_has ?) → (Σdst. fn_env_has … f dst ty) → Σf':partial_fn fx. fn_contains … f f' with
 [ Id t i ⇒ λEnv,dst.
-    let r ≝ lookup_reg env i t Env in
+    let r ≝ lookup_reg (fx_env fx) i t Env in
     match register_eq r dst with
     [ inl _ ⇒ «f, ?»
@@ -520 +530 @@
     let ❬f,r❭ ≝ choose_reg … e' f Env in
     let f ≝ add_fresh_to_graph … (St_op1 t' t op dst r) f ?? in
-    let f ≝ add_expr … env ? e' Env f «r, ?» in
+    let f ≝ add_expr … ? e' Env f «r, ?» in
       «pi1 … f, ?»
 | Op2 _ _ _ op e1 e2 ⇒ λEnv,dst.
@@ -526 +536 @@
     let ❬f,r2❭ ≝ choose_reg … e2 f (proj2 … Env) in
     let f ≝ add_fresh_to_graph … (St_op2 ??? op dst r1 r2) f ?? in
-    let f ≝ add_expr … env ? e2 (proj2 … Env) f «r2, ?» in
-    let f ≝ add_expr … env ? e1 (proj1 … Env) f «r1, ?» in
+    let f ≝ add_expr … ? e2 (proj2 … Env) f «r2, ?» in
+    let f ≝ add_expr … ? e1 (proj1 … Env) f «r1, ?» in
       «pi1 … f, ?»
 | Mem t e' ⇒ λEnv,dst.
     let ❬f,r❭ ≝ choose_reg … e' f Env in
     let f ≝ add_fresh_to_graph … (St_load t r dst) f ?? in
-    let f ≝ add_expr … env ? e' Env f «r,?» in
+    let f ≝ add_expr … ? e' Env f «r,?» in
       «pi1 … f, ?»
 | Cond _ _ _ e' e1 e2 ⇒ λEnv,dst.
     let resume_at ≝ pf_entry … f in
-    let f ≝ add_expr … env ? e2 (proj2 … Env) f dst in
+    let f ≝ add_expr … ? e2 (proj2 … Env) f dst in
     let lfalse ≝ pf_entry … f in
     let f ≝ add_fresh_to_graph … (λ_.St_skip resume_at) f ?? in
-    let f ≝ add_expr … env ? e1 (proj2 … (proj1 … Env)) f «dst, ?» in
+    let f ≝ add_expr … ? e1 (proj2 … (proj1 … Env)) f «dst, ?» in
     let ❬f,r❭ ≝ choose_reg … e' f ? in
     let f ≝ add_fresh_to_graph … (λltrue. St_cond r ltrue lfalse) f ?? in
-    let f ≝ add_expr … env ? e' (proj1 … (proj1 … Env)) f «r, ?» in
+    let f ≝ add_expr … ? e' (proj1 … (proj1 … Env)) f «r, ?» in
       «pi1 … f, ?»
 | Ecost _ l e' ⇒ λEnv,dst.
-    let f ≝ add_expr … env ? e' Env f dst in
+    let f ≝ add_expr … ? e' Env f dst in
     let f ≝ add_fresh_to_graph … (St_cost l) f ?? in
       «f, ?»
@@ -560 +570 @@
 | @(fn_con_env … (pi2 ?? r1)) repeat @fn_contains_step @I
 | @(fn_con_env … (pi2 ?? r2)) repeat @fn_contains_step @I
-| #l % [ % [ @(fn_con_env ??????? (pi2 ?? r1)) | @(pi2 ?? r2) ] | @(fn_con_env … (pi2 ?? dst)) ] repeat @fn_contains_step @I 
+| #l % [ % [ @(fn_con_env … (pi2 ?? r1)) | @(pi2 ?? r2) ] | @(fn_con_env … (pi2 ?? dst)) ] repeat @fn_contains_step @I 
 | #l #H whd % [ @H | @(fn_con_graph … (pi2 ?? lfalse)) repeat @fn_contains_step @I ]
 | @(π1 (π1 Env))
@@ -567 +577 @@
 ] qed.
 
-let rec add_exprs (le:label_env) (env:env) (es:list (𝚺t:typ.expr t)) (Env:All ? (exprtyp_present env) es)
-                  (dsts:list register) (pf:length … es = length … dsts) (f:partial_fn le env)
-                  (Hdsts:All2 ?? (λr,e. fn_env_has le env f r (eject' typ expr e)) dsts es) on es: Σf':partial_fn le env. fn_contains le env f f' ≝
+let rec add_exprs (fx:fixed) (es:list (𝚺t:typ.expr t)) (Env:All ? (exprtyp_present (fx_env fx)) es)
+                  (dsts:list register) (pf:length … es = length … dsts) (f:partial_fn fx)
+                  (Hdsts:All2 ?? (λr,e. fn_env_has … f r (eject' typ expr e)) dsts es) on es: Σf':partial_fn fx. fn_contains … f f' ≝
 match es return λes.All ?? es → All2 ???? es → |es|=|dsts| → ? with
-[ nil ⇒ λ_.λ_. match dsts return λx. ?=|x| → Σf':partial_fn le env. fn_contains le env f f' with [ nil ⇒ λ_. «f, ?» | cons _ _ ⇒ λpf.⊥ ]
+[ nil ⇒ λ_.λ_. match dsts return λx. ?=|x| → Σf':partial_fn fx. fn_contains … f f' with [ nil ⇒ λ_. «f, ?» | cons _ _ ⇒ λpf.⊥ ]
 | cons e et ⇒ λEnv.
-    match dsts return λx. All2 ?? (λr,e. fn_env_has le env f r (eject' typ expr e)) x (e::et) → ?=|x| → ? with
+    match dsts return λx. All2 ?? (λr,e. fn_env_has … f r (eject' typ expr e)) x (e::et) → ?=|x| → ? with
     [ nil ⇒ λ_.λpf.⊥
     | cons r rt ⇒ λHdsts,pf.
-        let f' ≝ add_exprs ? env et ? rt ? f ? in
-        match e return λe.exprtyp_present ? e → fn_env_has le env f r (eject' typ expr e) → ? with [ mk_DPair ty e ⇒ λEnv,Hr.
-          let f'' ≝ add_expr ? env ty e ? f' r in
+        let f' ≝ add_exprs … et ? rt ? f ? in
+        match e return λe.exprtyp_present ? e → fn_env_has … f r (eject' typ expr e) → ? with [ mk_DPair ty e ⇒ λEnv,Hr.
+          let f'' ≝ add_expr … ty e ? f' r in
             «pi1 … f'', ?»
         ] (proj1 ?? Env) (π1 Hdsts)
@@ -595 +605 @@
 axiom ReturnMismatch : String.
 
-definition stmt_inv : env → label_env → stmt → Prop ≝
-λenv,lenv. stmt_P (λs. stmt_vars (Env_has env) s ∧ stmt_labels (present ?? lenv) s).
+definition return_ok ≝
+λt,s. match s with [ St_return oe ⇒ rettyp_match t oe | _ ⇒ True ].
+
+record stmt_inv (fx:fixed) (s:stmt) : Prop ≝ {
+  si_vars : stmt_vars (Env_has (fx_env fx)) s;
+  si_labels : stmt_labels (present ?? (fx_lenv fx)) s;
+  si_return : return_ok (fx_rettyp fx) s
+}.
+
+definition stmts_inv : fixed → stmt → Prop ≝
+λfx. stmt_P (stmt_inv fx).
 
 (* Trick to avoid multiplying the proof obligations for the non-Id cases. *)
@@ -631 +650 @@
 qed.
 
-lemma empty_Cminor_labels_added : ∀le,env,s,f'.
-  labels_of s = [ ] → Cminor_labels_added le env s f'.
-#le #env #s #f' #E whd >E #l *;
-qed.
-
-lemma equal_Cminor_labels_added : ∀le,env,s,s',f.
+lemma empty_Cminor_labels_added : ∀fx,s,f'.
+  labels_of s = [ ] → Cminor_labels_added fx s f'.
+#fx #s #f' #E whd >E #l *;
+qed.
+
+lemma equal_Cminor_labels_added : ∀fx,s,s',f.
   labels_of s = labels_of s' → Cminor_labels_added … s' f →
-  Cminor_labels_added le env s f.
-#le #env #s #s' #f #E whd in ⊢ (% → %); > E #H @H
-qed.
-
-lemma Cminor_labels_con : ∀le,env,s,f,f'.
-  fn_contains le env f f' →
+  Cminor_labels_added fx s f.
+#fx #s #s' #f #E whd in ⊢ (% → %); > E #H @H
+qed.
+
+lemma Cminor_labels_con : ∀fx,s,f,f'.
+  fn_contains fx f f' →
   Cminor_labels_added … s f →
   Cminor_labels_added … s f'.
-#le #env #s #f #f' #INC #ADDED
+#fx #s #f #f' #INC #ADDED
 #l #E cases (ADDED l E) #l' * #L #P
 %{l'} % [ @L | @(present_included … P) @INC ]
 qed.
 
-lemma Cminor_labels_inv : ∀le,env,s,s',f.
-  ∀f':Σf':partial_fn le env. add_stmt_inv le env s' f f'.
-  Cminor_labels_added le env s f →
-  Cminor_labels_added le env s f'.
-#le #env #s #s' #f * #f' * #H1 #H2 #H3
+lemma Cminor_labels_inv : ∀fx,s,s',f.
+  ∀f':Σf':partial_fn fx. add_stmt_inv fx s' f f'.
+  Cminor_labels_added fx s f →
+  Cminor_labels_added fx s f'.
+#fx #s #s' #f * #f' * #H1 #H2 #H3
 #l #E cases (H3 l E) #l' * #L #P
 %{l'} % [ @L | @(present_included … P) @H1 ]
 qed.
 
-lemma Cminor_labels_sig : ∀le,env,s,f.
-  ∀f':Σf':partial_fn le env. fn_contains … f f'.
+lemma Cminor_labels_sig : ∀fx,s,f.
+  ∀f':Σf':partial_fn fx. fn_contains … f f'.
   Cminor_labels_added … s f →
   Cminor_labels_added … s f'.
-#le #env #s #f * #f' #H1 #H2
+#fx #s #f * #f' #H1 #H2
 #l #E cases (H2 l E) #l' * #L #P
 %{l'} % [ @L | @(present_included … P) @H1 ]
 qed.
 
-let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_inv env label_env s) (f:partial_fn label_env env) on s : res (Σf':partial_fn label_env env. add_stmt_inv label_env env s f f') ≝
-match s return λs.stmt_inv env label_env s → res (Σf':partial_fn label_env env. add_stmt_inv … s f f') with
+discriminator option.
+discriminator DPair.
+
+(* Return statements need a little careful treatment to avoid errors using the
+   invariant about the return type. *)
+
+definition add_return : ∀fx,opt_e. ∀f:partial_fn fx. ∀Env:stmts_inv fx (St_return opt_e).
+  Σf':partial_fn fx. add_stmt_inv fx (St_return opt_e) f f' ≝
+λfx,opt_e,f.
+  let f0 ≝ f in
+  let f ≝ add_fresh_to_graph … (λ_. R_return) f ?? in
+  match opt_e return λo. stmts_inv ? (St_return o) → Σf':partial_fn fx.add_stmt_inv … (St_return o) f0 f' with
+  [ None ⇒ λEnv. «pi1 … f, ?»
+  | Some et ⇒
+    match et return λe.stmts_inv fx (St_return (Some ? e)) → Σf':partial_fn fx.add_stmt_inv … (St_return (Some ? e)) f0 f' with
+    [ mk_DPair ty e ⇒ λEnv.
+      match fx_rettyp fx return λX. rettyp_match X ? → match X with [ Some t ⇒ Σr:register. env_has ?? t | None ⇒ ? ] → ? with
+      [ None ⇒ λH. ⊥
+      | Some t ⇒ λH,R.
+        match R with
+        [ mk_Sig r Hr ⇒ 
+            let f ≝ add_expr fx ty e ? f «r, ?» in
+            «pi1 … f, ?»
+        ]
+      ] (si_return … (π1 Env)) (pf_result fx f)
+    ]
+  ].
+[ @mk_add_stmt_inv /2/
+| inversion H #A #B #C destruct
+| @mk_add_stmt_inv
+  [ repeat @fn_contains_step @I
+  | @empty_Cminor_labels_added //
+  ]
+| @(si_vars … (π1 Env))
+| inversion H [ #E destruct ] #ty' #e' #E1 #E2 #_ destruct @Hr
+| #l #H @I
+| #l //
+] qed.
+
+
+let rec add_stmt (fx:fixed) (s:stmt) (Env:stmts_inv fx s) (f:partial_fn fx) on s : res (Σf':partial_fn fx. add_stmt_inv fx s f f') ≝
+match s return λs.stmts_inv fx s → res (Σf':partial_fn fx. add_stmt_inv … s f f') with
 [ St_skip ⇒ λ_. OK ? «f, ?»
 | St_assign t x e ⇒ λEnv.
-    let dst ≝ lookup_reg env x t (π1 (π1 Env)) in
-    OK ? «pi1 … (add_expr ? env ? e (π2 (π1 Env)) f dst), ?»
+    let dst ≝ lookup_reg (fx_env fx) x t (π1 (si_vars … (π1 Env))) in
+    OK ? «pi1 … (add_expr … e (π2 (si_vars … (π1 Env))) f dst), ?»
 | St_store t e1 e2 ⇒ λEnv.
-    let ❬f, val_reg❭ ≝ choose_reg … e2 f (π2 (π1 Env)) in
-    let ❬f, addr_reg❭ ≝ choose_reg … e1 f (π1 (π1 Env)) in
+    let ❬f, val_reg❭ ≝ choose_reg … e2 f (π2 (si_vars … (π1 Env))) in
+    let ❬f, addr_reg❭ ≝ choose_reg … e1 f (π1 (si_vars … (π1 Env))) in
     let f ≝ add_fresh_to_graph … (St_store t addr_reg val_reg) f ?? in
-    let f ≝ add_expr ? env ? e1 (π1 (π1 Env)) f «addr_reg, ?» in
-    OK ? «pi1 … (add_expr ? env ? e2 (π2 (π1 Env)) f «val_reg, ?»), ?»
+    let f ≝ add_expr … e1 (π1 (si_vars … (π1 Env))) f «addr_reg, ?» in
+    OK ? «pi1 … (add_expr … ? e2 (π2 (si_vars … (π1 Env))) f «val_reg, ?»), ?»
 | St_call return_opt_id e args ⇒ λEnv.
     let return_opt_reg ≝
       match return_opt_id return λo. ? → ? with
       [ None ⇒ λ_. None ?
-      | Some idty ⇒ λEnv. Some ? (lookup_reg env (\fst idty) (\snd idty) ?)
+      | Some idty ⇒ λEnv. Some ? (lookup_reg (fx_env fx) (\fst idty) (\snd idty) ?)
       ] Env in
-    let ❬f, args_regs❭ ≝ choose_regs ? env args f (π2 (π1 Env)) in
+    let ❬f, args_regs❭ ≝ choose_regs ? args f (π2 (si_vars ?? (π1 Env))) in
     let f ≝
       match expr_is_Id ? e with
       [ Some id ⇒ add_fresh_to_graph … (St_call_id id args_regs return_opt_reg) f ??
       | None ⇒ 
-        let ❬f, fnr❭ ≝ choose_reg … e f (π2 (π1 (π1 Env))) in
+        let ❬f, fnr❭ ≝ choose_reg … e f (π2 (π1 (si_vars … (π1 Env)))) in
         let f ≝ add_fresh_to_graph … (St_call_ptr fnr args_regs return_opt_reg) f ?? in
-        «pi1 … (add_expr ? env ? e (π2 (π1 (π1 Env))) f «fnr, ?»), ?»
+        «pi1 … (add_expr … ? e (π2 (π1 (si_vars … (π1 Env)))) f «fnr, ?»), ?»
       ] in
-    OK ? «pi1 … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f ?), ?»
+    OK ? «pi1 … (add_exprs … args (π2 (si_vars … (π1 Env))) args_regs ? f ?), ?»
 (*
 | St_tailcall e args ⇒ λEnv.
@@ -711 +770 @@
 *)
 | St_seq s1 s2 ⇒ λEnv.
-    do f2 ← add_stmt env label_env s2 ? f;
-    do f1 ← add_stmt env label_env s1 ? f2;
+    do f2 ← add_stmt … s2 ? f;
+    do f1 ← add_stmt … s1 ? f2;
       OK ? «pi1 … f1, ?»
 | St_ifthenelse _ _ e s1 s2 ⇒ λEnv.
     let l_next ≝ pf_entry … f in
-    do f2 ← add_stmt env label_env s2 (π2 Env) f;
+    do f2 ← add_stmt … s2 (π2 (π2 Env)) f;
     let l2 ≝ pf_entry … f2 in
     let f ≝ add_fresh_to_graph … (λ_. R_skip l_next) f2 ?? in
-    do f1 ← add_stmt env label_env s1 (π2 (π1 Env)) f;
-    let ❬f,r❭ ≝ choose_reg … e f1 (π1 (π1 (π1 Env))) in
+    do f1 ← add_stmt … s1 (π1 (π2 Env)) f;
+    let ❬f,r❭ ≝ choose_reg … e f1 (si_vars … (π1 Env)) in
     let f ≝ add_fresh_to_graph … (λl1. St_cond r l1 l2) f ?? in
-    OK ? «pi1 … (add_expr ? env ? e (π1 (π1 (π1 Env))) f «r, ?»), ?»
-| St_return opt_e ⇒ let f0 ≝ f in
+    OK ? «pi1 … (add_expr … ? e (si_vars … (π1 Env)) f «r, ?»), ?»
+| St_return opt_e ⇒ λEnv. OK ? (add_return fx opt_e f Env)
+(*let f0 ≝ f in
     let f ≝ add_fresh_to_graph … (λ_. R_return) f ?? in
-    match opt_e return λo. stmt_inv ?? (St_return o) → res (Σf':partial_fn label_env env.add_stmt_inv … (St_return o) f0 f') with
+    match opt_e return λo. stmt_inv ? (St_return o) → res (Σf':partial_fn fx.add_stmt_inv … (St_return o) f0 f') with
     [ None ⇒ λEnv. OK ? «pi1 … f, ?»
     | Some e ⇒ 
-        match pf_result … f with
+        match fx_rettyp … f with
         [ None ⇒ λEnv. Error ? (msg ReturnMismatch)
         | Some r ⇒ 
-            match e return λe.stmt_inv env label_env (St_return (Some ? e)) → res (Σf':partial_fn label_env env.add_stmt_inv … (St_return (Some ? e)) f0 f') with
+            match e return λe.stmt_inv fx (St_return (Some ? e)) → res (Σf':partial_fn fx.add_stmt_inv … (St_return (Some ? e)) f0 f') with
             [ mk_DPair ty e ⇒ λEnv.
                 match typ_eq (\snd r) ty with
-                [ inl E ⇒ let f ≝ add_expr label_env env ty e ? f «\fst r, ? E (* XXX E goes missing if I don't use it! *)» in
+                [ inl E ⇒ let f ≝ add_expr … ty e ? f «\fst r, ? E (* XXX E goes missing if I don't use it! *)» in
                           OK ? «pi1 … f, ?»
                 | inr _ ⇒ Error ? (msg ReturnMismatch)
@@ -740 +800 @@
             ]
         ]
-    ]
+    ]*)
 | St_label l s' ⇒ λEnv.
-    do f ← add_stmt env label_env s' (π2 Env) f;
-    let l' ≝ lookup_label label_env l ? in
+    do f ← add_stmt … s' (π2 Env) f;
+    let l' ≝ lookup_label (fx_lenv fx) l ? in
     OK ? «pi1 … (add_to_graph … l' (R_skip (pf_entry … f)) f ??), ?»
 | St_goto l ⇒ λEnv.
-    let l' ≝ lookup_label label_env l ? in
+    let l' ≝ lookup_label (fx_lenv fx) l ? in
     OK ? «pi1 … (add_fresh_to_graph' … (λ_.R_skip l') f ??), ?»
 | St_cost l s' ⇒ λEnv.
-    do f ← add_stmt env label_env s' (π2 Env) f;
+    do f ← add_stmt … s' (π2 Env) f;
     OK ? «pi1 … (add_fresh_to_graph … (St_cost l) f ??), ?»
 ] Env.
-try @(π1 Env)
 try @(π2 Env)
-try @(π1 (π1 Env))
-try @(π2 (π1 Env))
+try @(π1 (π2 Env))
+try @(π2 (π2 Env))
 try @mk_add_stmt_inv
 try (repeat @fn_contains_step @I)
@@ -762 +821 @@
 try (#l #H @H)
 try (#l @I)
-[ @(pf_envok … (π1 (π1 Env))) @refl
+[ @(pf_envok … (π1 (si_vars … (π1 Env)))) @refl
 | @(fn_con_env … (pi2 ?? val_reg)) repeat @fn_contains_step @I
 | @(fn_con_env … (pi2 ?? addr_reg)) repeat @fn_contains_step @I
@@ -768 +827 @@
 | @sym_eq @(All2_length … (pi2 ?? args_regs))
 | @(fn_con_env … (pi2 ?? fnr)) repeat @fn_contains_step @I
-| @(π1 (π1 (π1 Env)))
+| @(π1 (π1 (si_vars … (π1 Env))))
 | #l #H cases (Exists_append … H)
-  [ #H1 @(stmt_labels_added ????? (pi2 ?? f1) ? H1)
-  | #H2 @(Cminor_labels_inv … H2) @(stmt_labels_added ????? (pi2 ?? f2))
+  [ #H1 @(stmt_labels_added ???? (pi2 ?? f1) ? H1)
+  | #H2 @(Cminor_labels_inv … H2) @(stmt_labels_added ???? (pi2 ?? f2))
   ]
 | #l #H @(fn_con_graph … (pi2 ?? l_next)) repeat @fn_contains_step @I
 | #l #H cases (Exists_append … H)
-  [ #H1 @(Cminor_labels_sig … H1) @Cminor_labels_sig @Cminor_labels_sig @(stmt_labels_added ????? (pi2 ?? f1)) 
-  | #H2 @(Cminor_labels_sig … H2) @Cminor_labels_sig @Cminor_labels_sig @Cminor_labels_inv @Cminor_labels_sig @(stmt_labels_added ????? (pi2 ?? f2)) 
+  [ #H1 @(Cminor_labels_sig … H1) @Cminor_labels_sig @Cminor_labels_sig @(stmt_labels_added ???? (pi2 ?? f1)) 
+  | #H2 @(Cminor_labels_sig … H2) @Cminor_labels_sig @Cminor_labels_sig @Cminor_labels_inv @Cminor_labels_sig @(stmt_labels_added ???? (pi2 ?? f2)) 
   ]
 | @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
 | #l #H % [ @H | @(fn_con_graph … (pi2 ?? l2)) repeat @fn_contains_step @I ]
-| #_ (* see above *) <E @(pi2 ?? r)
+| @(si_labels … (π1 Env))
 | @(pi2 … (pf_entry …))
 | #l1 * [ #E >E %{l'} % [ @lookup_label_rev' | whd >lookup_add_hit % #E' destruct (E') ]
-        | @Cminor_labels_sig @(stmt_labels_added ????? (pi2 … f))
+        | @Cminor_labels_sig @(stmt_labels_added ???? (pi2 … f))
         ]
 | #l1 #H whd %2 @lookup_label_lpresent
-| @(equal_Cminor_labels_added ??? s') [ @refl | @Cminor_labels_sig @(stmt_labels_added ????? (pi2 … f)) ]
+| @(si_labels … (π1 Env))
+| @(equal_Cminor_labels_added ?? s') [ @refl | @Cminor_labels_sig @(stmt_labels_added ???? (pi2 … f)) ]
 ] qed.
 
@@ -797 +857 @@
 let 〈locals0, env, reggen2〉 as E2 ≝ populate_env env1 reggen1 (f_vars f) in
 let ❬locals_reggen, result❭ as E3 ≝
-  match f_return f return λ_.𝚺lr. option (Σrt. env_has ((\fst lr)@params) (\fst rt) (\snd rt)) with
-  [ None ⇒ ❬〈locals0, reggen2〉, None ?❭
+  match f_return f return λt.𝚺lr. resultok t ((\fst lr)@params) with
+  [ None ⇒ ❬〈locals0, reggen2〉, I❭
   | Some ty ⇒
       let 〈r,gen〉 ≝ fresh … reggen2 in
-        mk_DPair ? (λlr.option (Σrt. env_has ((\fst lr)@params) (\fst rt) (\snd rt))) 〈〈r,ty〉::locals0, gen〉 (Some ? «〈r,ty〉, ?») ] in
+        mk_DPair ? (λlr.Σr. env_has ((\fst lr)@params) r ty) 〈〈r,ty〉::locals0, gen〉 «r, ?» ] in
 let locals ≝ \fst locals_reggen in
 let reggen ≝ \snd locals_reggen in
 let 〈label_env, labgen1〉 as El ≝ populate_label_env (empty_map …) labgen0 cminor_labels in
 let 〈l,labgen〉 ≝ fresh … labgen1 in
+let fixed ≝ mk_fixed label_env env (f_return f) in
 let emptyfn ≝
-  mk_partial_fn
-    label_env
-    env
+  mk_partial_fn fixed
     labgen
     reggen
@@ -822 +881 @@
     l
     l in
-do f ← add_stmt env label_env (f_body f) ? emptyfn;
+do f ← add_stmt fixed (f_body f) ? emptyfn;
 OK ? (mk_internal_function
     (pf_labgen … f)
     (pf_reggen … f)
-    (match pf_result … f with [ None ⇒ None ? | Some rt ⇒ Some ? (pi1 … rt) ])
+    (match fx_rettyp fixed return λt. match t with [ Some t ⇒ Σr:register. env_has ? r t | _ ⇒ True ] → ? with [ None ⇒ λ_. None ? | Some t ⇒ λR. Some ? 〈(pi1 … R),t〉 ] (pf_result … f))
     (pf_params … f)
     (pf_locals … f)
@@ -849 +908 @@
   | @(stmt_labels_mp … L)
     #l #H @(populates_label_env … (sym_eq … El)) @H
+  | cases s in R ⊢ %; //
   ]
 | #l #s #E @(labels_P_mp … (pf_closed … f l s E))
@@ -864 +924 @@
   [ * #H1 #L1 cases (populate_env_list … (sym_eq … E1) … H1 L1)
     [ * * | normalize @Exists_append_r ]
-  | cases (f_return f) in E3;
-    [ whd in ⊢ (??%% → ?); #E3 whd in match locals; destruct
+  | (* gave up with     cases (f_return f) in result E3; *)
+    @(match f_return f return λx.∀R:resultok x ((\fst locals_reggen)@params). ❬locals_reggen,R❭ = match x with [None ⇒ ?|Some _ ⇒ ?] → ? with [ None ⇒ λres1.? | Some rty ⇒ λres1.?] result E3)
+    [ whd in ⊢ (??%% → ?); #E3' whd in match locals; destruct
       @Exists_append_l
-    | #rt cases (fresh ? reggen2) #rr #ru whd in ⊢ (??%% → ?); #E3 whd in match locals; destruct
+    | cases (fresh ? reggen2) #rr #ru whd in ⊢ (??%% → ?); #E3' whd in match locals; destruct
       #H' @Exists_append_l %2 @H'
     ]