source: etc/campbell/dev-notes/2012-10-09-cost-labels-in-syntax.patch

Deliverables/D2.2/8051-matita-out/src/clight/clightPrintMatita.ml

@@ -265 +265 @@
               print_stmt s1
               print_stmt s2
   | Swhile(_, e, s) ->
-      fprintf p "@[<v 2>(Swhile %a@ %a)@]"
+      fprintf p "@[<v 2>(Swhile %a@ (None ?)@ %a@ (None ?))@]"
               print_expr e
               print_stmt s
   | Sdowhile(_, e, s) ->
-      fprintf p "@[<v 2>S(dowhile %a@ %a)@]"
+      fprintf p "@[<v 2>S(dowhile %a@ (None ?)@ %a@ (None ?))@]"
               print_expr e
               print_stmt s
   | Sfor(_, s_init, e, s_iter, s_body) ->
-      fprintf p "@[<v 2>(Sfor %a@ %a@ %a@\n%a@;<0 -2>)@]"
+      fprintf p "@[<v 2>(Sfor %a@ %a@ %a@ (None ?)@\n%a@;<0 -2>(None ?))@]"
               print_stmt s_init
               print_expr e
               print_stmt s_iter

src/CHANGES

@@ -87 +87 @@
   to be used in is_final. In Matita, they don't. For RTL the information was
   duplicated in the internal function record. I have done the same for ERTL too.
   To be double checked with the OCaml semantics.
+
+02/10/2012:
+  Cost labels following loops and for the body of each loop have been
+  incorporated into the syntax of Swhile, etc.  This keeps them closely
+  associated with the loop, allowing us to avoid placing skips before cost
+  labels which breaks our labelling invariant.  The Cminor to RTLabs translation
+  is also careful to avoid introducing skips at goto labels for the same reason,
+  by backpatching the gotos after the rest of the code is generated.

src/Clight/Cexec.ma

@@ -330 +330 @@
 λs.match s return λs'.(s' = Sskip) ⊎ (s' ≠ Sskip) with
 [ Sskip ⇒ inl ?? (refl ??)
 | _ ⇒ inr ?? (nmk ? (λH.?))
-]. destruct
+]. lapply (eq_to_jmeq ??? H) -H #H destruct
 qed.
 
 
@@ -389 +389 @@
           [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉
           | _ ⇒ Wrong ??? (msg NonsenseState)
           ]
-      | Kwhile a s' cl k' ⇒ ret ? 〈E0, State f (Swhile a s' cl) k' e m〉
-      | Kdowhile a s' k' ⇒
+      | Kwhile a lb s' lp k' ⇒ ret ? 〈E0, State f (Swhile a lb s' lp) k' e m〉
+      | Kdowhile a lb s' lp k' ⇒
           ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
           ! b ← err_to_io … (exec_bool_of_val v (typeof a));
           match b with
-          [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
-          | false ⇒ ret ? 〈tr, State f Sskip k' e m〉
+          [ true ⇒ ret ? 〈tr, State f (Sdowhile a lb s' lp) k' e m〉
+          | false ⇒ ret ? 〈tr, State f (optional_cost lp Sskip) k' e m〉
           ]
-      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉
-      | Kfor3 a2 a3 s' k' ⇒ ret ? 〈E0, State f (Sfor Sskip a2 a3 s') k' e m〉
+      | Kfor2 a2 a3 lb s' lp k' ⇒ ret ? 〈E0, State f a3 (Kfor3 a2 a3 lb s' lp k') e m〉
+      | Kfor3 a2 a3 lb s' lp k' ⇒ ret ? 〈E0, State f (Sfor Sskip a2 a3 lb s' lp) k' e m〉
       | Kswitch k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
       | _ ⇒ Wrong ??? (msg NonsenseState)
       ]
   | Scontinue ⇒
       match k with
       [ Kseq s' k' ⇒ ret ? 〈E0, State f Scontinue k' e m〉
-      | Kwhile a s' cl k' ⇒ ret ? 〈E0, State f (Swhile a s' cl) k' e m〉
-      | Kdowhile a s' k' ⇒ 
+      | Kwhile a lb s' lp k' ⇒ ret ? 〈E0, State f (Swhile a lb s' lp) k' e m〉
+      | Kdowhile a lb s' lp k' ⇒ 
           ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
           ! b ← err_to_io … (exec_bool_of_val v (typeof a));
           match b with
-          [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
-          | false ⇒ ret ? 〈tr, State f Sskip k' e m〉
+          [ true ⇒ ret ? 〈tr, State f (Sdowhile a lb s' lp) k' e m〉
+          | false ⇒ ret ? 〈tr, State f (optional_cost lp Sskip) k' e m〉
           ]
-      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉
+      | Kfor2 a2 a3 lb s' lp k' ⇒ ret ? 〈E0, State f a3 (Kfor3 a2 a3 lb s' lp k') e m〉
       | Kswitch k' ⇒ ret ? 〈E0, State f Scontinue k' e m〉
       | _ ⇒ Wrong ??? (msg NonsenseState)
       ]
   | Sbreak ⇒
       match k with
       [ Kseq s' k' ⇒ ret ? 〈E0, State f Sbreak k' e m〉
-      | Kwhile a s' cl k' ⇒ ret ? 〈E0, State f (optional_cost cl Sskip) k' e m〉
-      | Kdowhile a s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
-      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
+      | Kwhile a lb s' lp k' ⇒ ret ? 〈E0, State f (optional_cost lp Sskip) k' e m〉
+      | Kdowhile a lb s' lp k' ⇒ ret ? 〈E0, State f (optional_cost lp Sskip) k' e m〉
+      | Kfor2 a2 a3 lb s' lp k' ⇒ ret ? 〈E0, State f (optional_cost lp Sskip) k' e m〉
       | Kswitch k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
       | _ ⇒ Wrong ??? (msg NonsenseState)
       ]
@@ -430 +430 @@
       ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
       ! b ← err_to_io … (exec_bool_of_val v (typeof a));
       ret ? 〈tr, State f (if b then s1 else s2) k e m〉
-  | Swhile a s' cl ⇒ 
+  | Swhile a lb s' lp ⇒ 
       ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
       ! b ← err_to_io … (exec_bool_of_val v (typeof a));
-      ret ? 〈tr, if b then State f s' (Kwhile a s' cl k) e m
-                      else State f (optional_cost cl Sskip) k e m〉
-  | Sdowhile a s' ⇒ ret ? 〈E0, State f s' (Kdowhile a s' k) e m〉
-  | Sfor a1 a2 a3 s' ⇒
+      ret ? 〈tr, if b then State f (optional_cost lb s') (Kwhile a lb s' lp k) e m
+                      else State f (optional_cost lp Sskip) k e m〉
+  | Sdowhile a lb s' lp ⇒ ret ? 〈E0, State f (optional_cost lb s') (Kdowhile a lb s' lp k) e m〉
+  | Sfor a1 a2 a3 lb s' lp ⇒
       match is_Sskip a1 with
       [ inl _ ⇒ 
           ! 〈v,tr〉 ← exec_expr ge e m a2 : IO ???;
           ! b ← err_to_io … (exec_bool_of_val v (typeof a2));
-          ret ? 〈tr, State f (if b then s' else Sskip) (if b then (Kfor2 a2 a3 s' k) else k) e m〉
-      | inr _ ⇒ ret ? 〈E0, State f a1 (Kseq (Sfor Sskip a2 a3 s') k) e m〉
+          ret ? 〈tr, State f (if b then optional_cost lb s' else optional_cost lp Sskip) (if b then (Kfor2 a2 a3 lb s' lp k) else k) e m〉
+      | inr _ ⇒ ret ? 〈E0, State f a1 (Kseq (Sfor Sskip a2 a3 lb s' lp) k) e m〉
       ]
   | Sreturn a_opt ⇒
     match a_opt with

src/Clight/CexecComplete.ma

@@ -382 +382 @@
     >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
     >(yields_eq ??? (bool_of_false ?? H2))
     @refl
-| #f #e #s #cl #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
+| #f #e #lb #s #lp #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
     >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
     >(yields_eq ??? (bool_of_false ?? H2))
     @refl
-| #f #e #s #cl #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
+| #f #e #lb #s #lp #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
     >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
     >(yields_eq ??? (bool_of_true ?? H2))
     @refl
-| #f #s1 #e #s2 #cl #k #env #m #H cases H; #es1 >es1 @refl
-| 13,14: #f #e #s [#cl] #k #env #m @refl
-| #f #s1 #e #s2 #k #env #m #v #tr *; #es1 >es1 #H1 #H2 whd in ⊢ (??%?);
+| #f #s1 #e #lb #s2 #lp #k #env #m #H cases H; #es1 >es1 @refl
+| 13,14: #f #e #lb #s #lp #k #env #m @refl
+| #f #s1 #e #lb #s2 #lp #k #env #m #v #tr *; #es1 >es1 #H1 #H2 whd in ⊢ (??%?);
     >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
     >(yields_eq ??? (bool_of_false ?? H2))
     @refl
-| #f #s1 #e #s2 #k #env #m #v #tr *; #es1 >es1 #H1 #H2 whd in ⊢ (??%?);
+| #f #s1 #e #lb #s2 #lp #k #env #m #v #tr *; #es1 >es1 #H1 #H2 whd in ⊢ (??%?);
     >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
     >(yields_eq ??? (bool_of_true ?? H2))
     @refl
-| #f #e #s #k #env #m @refl
-| #f #s1 #e #s2 #s3 #k #env #m #nskip whd in ⊢ (??%?); cases (is_Sskip s1);
+| #f #e #lb #s #lp #k #env #m @refl
+| #f #s1 #e #s2 #lb #s3 #lp #k #env #m #nskip whd in ⊢ (??%?); cases (is_Sskip s1);
     [ #H @False_ind @(absurd ? H nskip)
     | #H whd in ⊢ (??%?); @refl ]
-| #f #e #s1 #s2 #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
+| #f #e #s1 #lb #s2 #lp #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
     >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
     >(yields_eq ??? (bool_of_false ?? H2))
     @refl
-| #f #e #s1 #s2 #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
+| #f #e #s1 #lb #s2 #lp #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
     >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
     >(yields_eq ??? (bool_of_true ?? H2))
     @refl
-| #f #s1 #e #s2 #s3 #k #env #m *; #es1 >es1 @refl
-| 22,23: #f #e #s1 #s2 #k #env #m @refl
+| #f #s1 #e #s2 #lb #s3 #lp #k #env #m *; #es1 >es1 @refl
+| 22,23: #f #e #s1 #lb #s2 #lp #k #env #m @refl
 | #f #k #env #m #H whd in ⊢ (??%?); >H @refl
 | #f #e #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
     @(dec_false ? (type_eq_dec (fn_return f) Tvoid) H1) #pf'
@@ -423 +423 @@
 | #f #k #env #m cases k;
     [ #H1 #H2 whd in ⊢ (??%?); >H2 @refl
     | #s' #k' whd in ⊢ (% → ?); *;
-    | 3,4: #e' #s' [#cl] #k' whd in ⊢ (% → ?); *;
-    | 5,6: #e' #s1' #s2' #k' whd in ⊢ (% → ?); *;
+    | 3,4: #e' #lb #s' #lp #k' whd in ⊢ (% → ?); *;
+    | 5,6: #e' #s1' #lb #s2' #lp #k' whd in ⊢ (% → ?); *;
     | #k' whd in ⊢ (% → ?); *;
     | #r #f' #env' #k' #H1 #H2 whd in ⊢ (??%?); >H2 @refl
     ]

src/Clight/CexecEquiv.ma

@@ -513 +513 @@
   ∀ge,s. interact_prop ? (λo,k. ∀i.∃tr.∃s'. k i = Value ??? 〈tr,s'〉 ∧ tr ≠ E0) (exec_step ge s).
 #ge #s cases s;
 [ #f #st #kk #e #m cases st;
-  [ 11,14: #a | 2,4,7,12,13,15: #a #b | 3,5,6: #a #b #c | 8: #a #b #c #d ]
-  [ 4,5,7,8: @I ]
+  [ 11,14: #a | 2,4,12,13,15: #a #b | 3,5: #a #b #c | 6,7: #a #b #c #d | 8: #a #b #c #d #e #f ]
+  try @I
   whd in ⊢ (???%);
   [ cases a; [ cases (fn_return f); //; | #e whd nodelta in ⊢ (???%);
                     cases (type_eq_dec (fn_return f) Tvoid); #x //; @err2_does_not_interact // ]
@@ -527 +527 @@
   | cases (is_Sskip a); #H [ @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 @I
       | @I ]
   | cases kk; [ 1,8: cases (fn_return f); //; | 2,3,5,6,7: //;
-      | #z1 #z2 #z3 @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 cases x3; @I ]
+      | #z1 #z2 #z3 #z4 #z5 @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 cases x3; @I ]
   | cases kk; //;
-  | cases kk; [ 4: #z1 #z2 #z3  @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 cases x3; @I
+  | cases kk; [ 4: #z1 #z2 #z3 #z4 #z5 @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 cases x3; @I
       | *: // ]
   ]
 | #f #args #kk #m cases f; 

src/Clight/CexecSound.ma

@@ -336 +336 @@
         //; #H whd;
         @step_skip_call //;
     | #s' #k' whd; //
-    | #ex #s' #cl #k' @step_skip_or_continue_while % //;
-    | #ex #s' #k'
+    | #ex #lb #s' #lp #k' @step_skip_or_continue_while % //;
+    | #ex #lb #s' #lp #k'
         @res_bindIO2_OK #v #tr #Hv
         letin bexpr ≝ (exec_bool_of_val v (typeof ex));
         lapply (refl ? bexpr);
@@ -351 +351 @@
             ]
         | #msg #_ //;
         ]
-    | #ex #s1 #s2 #k' @step_skip_or_continue_for2 % //;
-    | #ex #s1 #s2 #k' @step_skip_for3
+    | #ex #s1 #lb #s2 #lp #k' @step_skip_or_continue_for2 % //;
+    | #ex #s1 #lb #s2 #lp #k' @step_skip_for3
     | #k' @step_skip_break_switch % //;
     | #r #f' #e' #k' whd in ⊢ (?????%);
         lapply (refl ? (fn_return f)); cases (fn_return f) in ⊢ (???% → %);
@@ -384 +384 @@
     [ @(step_ifthenelse_true … (exec_expr_sound' … Hv)) @(bool_of … Hb)
     | @(step_ifthenelse_false … (exec_expr_sound' … Hv)) @(bool_of … Hb)
     ]
-  | #ex #s' #cl
+  | #ex #lb #s' #lp
     @res_bindIO2_OK #v #tr #Hv
     letin bexpr ≝ (exec_bool_of_val v (typeof ex));
     lapply (refl ? bexpr); cases bexpr in ⊢ (???% → %); //;
@@ -392 +392 @@
     [ @(step_while_true … (exec_expr_sound' … Hv)) @(bool_of … Hb)
     | @(step_while_false … (exec_expr_sound' … Hv)) @(bool_of … Hb)
     ]
-  | #ex #s' // 
-  | #s1 #ex #s2 #s3 whd in ⊢ (?????%); elim (is_Sskip s1); #Hs1 whd in ⊢ (?????%);
+  | #ex #lb #s' #lp // 
+  | #s1 #ex #s2 #lb #s3 #lp whd in ⊢ (?????%); elim (is_Sskip s1); #Hs1 whd in ⊢ (?????%);
     [ >Hs1
       @res_bindIO2_OK #v #tr #Hv
       letin bexpr ≝ (exec_bool_of_val v (typeof ex));
@@ -406 +406 @@
     ]
   | whd in ⊢ (?????%); cases k; // #k' @step_skip_break_switch %2 //
   | whd in ⊢ (?????%); cases k; //;
-    [ #ex #s' #cl #k' whd; @step_skip_or_continue_while %2 ; //;
-    | #ex #s' #k' whd; 
+    [ #ex #lb #s' #lp #k' whd; @step_skip_or_continue_while %2 ; //;
+    | #ex #lb #s' #lp #k' whd; 
       @res_bindIO2_OK #v #tr #Hv
       letin bexpr ≝ (exec_bool_of_val v (typeof ex));
       lapply (refl ? bexpr); cases bexpr in ⊢ (???% → %); //;
@@ -417 +417 @@
       | @(step_skip_or_continue_dowhile_false … (exec_expr_sound' … Hv))
         [ %2 ; // | @(bool_of … Hb) ]
       ]
-    | #ex #s1 #s2 #k' whd; @step_skip_or_continue_for2 %2 ; //
+    | #ex #s1 #lb #s2 #lp #k' whd; @step_skip_or_continue_for2 %2 ; //
     ]
   | #r whd in ⊢ (?????%); cases r;
     [ whd; lapply (refl ? (fn_return f)); cases (fn_return f) in ⊢ (???% → %); //; #H

src/Clight/Csem.ma

@@ -907 +907 @@
 
 inductive cont: Type[0] :=
   | Kstop: cont
-  | Kseq: statement -> cont -> cont
+  | Kseq: statement → cont → cont
        (**r [Kseq s2 k] = after [s1] in [s1;s2] *)
-  | Kwhile: expr -> statement → option costlabel -> cont -> cont
-       (**r [Kwhile e s k] = after [s] in [while (e) s] *)
-  | Kdowhile: expr -> statement -> cont -> cont
-       (**r [Kdowhile e s k] = after [s] in [do s while (e)] *)
-  | Kfor2: expr -> statement -> statement -> cont -> cont
-       (**r [Kfor2 e2 e3 s k] = after [s] in [for(e1;e2;e3) s] *)
-  | Kfor3: expr -> statement -> statement -> cont -> cont
-       (**r [Kfor3 e2 e3 s k] = after [e3] in [for(e1;e2;e3) s] *)
-  | Kswitch: cont -> cont
+  | Kwhile: expr → option costlabel → statement → option costlabel → cont → cont
+       (**r [Kwhile e lb s lp k] = after [s] in [while (e) s] *)
+  | Kdowhile: expr → option costlabel → statement → option costlabel → cont → cont
+       (**r [Kdowhile e lb s lp k] = after [s] in [do s while (e)] *)
+  | Kfor2: expr → statement → option costlabel → statement → option costlabel → cont → cont
+       (**r [Kfor2 e2 e3 lb s lp k] = after [s] in [for(e1;e2;e3) s] *)
+  | Kfor3: expr → statement → option costlabel → statement → option costlabel → cont → cont
+       (**r [Kfor3 e2 e3 lb s lp k] = after [e3] in [for(e1;e2;e3) s] *)
+  | Kswitch: cont → cont
        (**r catches [break] statements arising out of [switch] *)
-  | Kcall: option (block × offset × type) -> (**r where to store result *)
-           function ->                       (**r calling function *)
-           env ->                            (**r local env of calling function *)
-           cont -> cont.
+  | Kcall: option (block × offset × type) → (**r where to store result *)
+           function →                       (**r calling function *)
+           env →                            (**r local env of calling function *)
+           cont → cont.
 
 (* * Pop continuation until a call or stop *)
 
 let rec call_cont (k: cont) : cont :=
   match k with
   [ Kseq s k => call_cont k
-  | Kwhile e s l k => call_cont k
-  | Kdowhile e s k => call_cont k
-  | Kfor2 e2 e3 s k => call_cont k
-  | Kfor3 e2 e3 s k => call_cont k
+  | Kwhile e _ s _ k => call_cont k
+  | Kdowhile e _ s _ k => call_cont k
+  | Kfor2 e2 e3 _ s _ k => call_cont k
+  | Kfor3 e2 e3 _ s _ k => call_cont k
   | Kswitch k => call_cont k
   | _ => k
   ].
@@ -982 +982 @@
       [ Some sk => Some ? sk
       | None => find_label lbl s2 k
       ]
-  | Swhile a s1 l =>
-      find_label lbl s1 (Kwhile a s1 l k)
-  | Sdowhile a s1 =>
-      find_label lbl s1 (Kdowhile a s1 k)
-  | Sfor a1 a2 a3 s1 =>
-      match find_label lbl a1 (Kseq (Sfor Sskip a2 a3 s1) k) with
+  | Swhile a lb s1 lp =>
+      find_label lbl s1 (Kwhile a lb s1 lp k)
+  | Sdowhile a lb s1 lp =>
+      find_label lbl s1 (Kdowhile a lb s1 lp k)
+  | Sfor a1 a2 a3 lb s1 lp =>
+      match find_label lbl a1 (Kseq (Sfor Sskip a2 a3 lb s1 lp) k) with
       [ Some sk => Some ? sk
       | None =>
-          match find_label lbl s1 (Kfor2 a2 a3 s1 k) with
+          match find_label lbl s1 (Kfor2 a2 a3 lb s1 lp k) with
           [ Some sk => Some ? sk
-          | None => find_label lbl a3 (Kfor3 a2 a3 s1 k)
+          | None => find_label lbl a3 (Kfor3 a2 a3 lb s1 lp k)
           ]
       ]
   | Sswitch e sl =>
@@ -1034 +1034 @@
 | Tcomp_ptr a ⇒ Tcomp_ptr a
 ].
 
+(* For loops we may generate a cost label statement for the body / following
+   code if there's one present in the loop statement. *)
+
 definition optional_cost : option costlabel → statement → statement ≝
 λo,s. match o with [ Some cl ⇒ Scost cl s | None ⇒ s ].
 
@@ -1089 +1092 @@
       step ge (State f (Sifthenelse a s1 s2) k e m)
            tr (State f s2 k e m)
 
-  | step_while_false: ∀f,a,s,cl,k,e,m,v,tr.
+  | step_while_false: ∀f,a,lb,s,lp,k,e,m,v,tr.
       eval_expr ge e m a v tr →
       is_false v (typeof a) →
-      step ge (State f (Swhile a s cl) k e m)
-           tr (State f (optional_cost cl Sskip) k e m)
-  | step_while_true: ∀f,a,s,cl,k,e,m,v,tr.
+      step ge (State f (Swhile a lb s lp) k e m)
+           tr (State f (optional_cost lp Sskip) k e m)
+  | step_while_true: ∀f,a,lb,s,lp,k,e,m,v,tr.
       eval_expr ge e m a v tr →
       is_true v (typeof a) →
-      step ge (State f (Swhile a s cl) k e m)
-           tr (State f s (Kwhile a s cl k) e m)
-  | step_skip_or_continue_while: ∀f,x,a,s,cl,k,e,m.
+      step ge (State f (Swhile a lb s lp) k e m)
+           tr (State f (optional_cost lb s) (Kwhile a lb s lp k) e m)
+  | step_skip_or_continue_while: ∀f,x,a,lb,s,lp,k,e,m.
       x = Sskip ∨ x = Scontinue →
-      step ge (State f x (Kwhile a s cl k) e m)
-           E0 (State f (Swhile a s cl) k e m)
-  | step_break_while: ∀f,a,s,cl,k,e,m.
-      step ge (State f Sbreak (Kwhile a s cl k) e m)
-           E0 (State f (optional_cost cl Sskip) k e m)
-
-  | step_dowhile: ∀f,a,s,k,e,m.
-      step ge (State f (Sdowhile a s) k e m)
-        E0 (State f s (Kdowhile a s k) e m)
-  | step_skip_or_continue_dowhile_false: ∀f,x,a,s,k,e,m,v,tr.
+      step ge (State f x (Kwhile a lb s lp k) e m)
+           E0 (State f (Swhile a lb s lp) k e m)
+  | step_break_while: ∀f,a,lb,s,lp,k,e,m.
+      step ge (State f Sbreak (Kwhile a lb s lp k) e m)
+           E0 (State f (optional_cost lp Sskip) k e m)
+
+  | step_dowhile: ∀f,a,lb,s,lp,k,e,m.
+      step ge (State f (Sdowhile a lb s lp) k e m)
+        E0 (State f (optional_cost lb s) (Kdowhile a lb s lp k) e m)
+  | step_skip_or_continue_dowhile_false: ∀f,x,a,lb,s,lp,k,e,m,v,tr.
       x = Sskip ∨ x = Scontinue →
       eval_expr ge e m a v tr →
       is_false v (typeof a) →
-      step ge (State f x (Kdowhile a s k) e m)
-           tr (State f Sskip k e m)
-  | step_skip_or_continue_dowhile_true: ∀f,x,a,s,k,e,m,v,tr.
+      step ge (State f x (Kdowhile a lb s lp k) e m)
+           tr (State f (optional_cost lp Sskip) k e m)
+  | step_skip_or_continue_dowhile_true: ∀f,x,a,lb,s,lp,k,e,m,v,tr.
       x = Sskip ∨ x = Scontinue →
       eval_expr ge e m a v tr →
       is_true v (typeof a) →
-      step ge (State f x (Kdowhile a s k) e m)
-           tr (State f (Sdowhile a s) k e m)
-  | step_break_dowhile: ∀f,a,s,k,e,m.
-      step ge (State f Sbreak (Kdowhile a s k) e m)
-           E0 (State f Sskip k e m)
+      step ge (State f x (Kdowhile a lb s lp k) e m)
+           tr (State f (Sdowhile a lb s lp) k e m)
+  | step_break_dowhile: ∀f,a,lb,s,lp,k,e,m.
+      step ge (State f Sbreak (Kdowhile a lb s lp k) e m)
+           E0 (State f (optional_cost lp Sskip) k e m)
 
-  | step_for_start: ∀f,a1,a2,a3,s,k,e,m.
+  | step_for_start: ∀f,a1,a2,a3,lb,s,lp,k,e,m.
       a1 ≠ Sskip →
-      step ge (State f (Sfor a1 a2 a3 s) k e m)
-           E0 (State f a1 (Kseq (Sfor Sskip a2 a3 s) k) e m)
-  | step_for_false: ∀f,a2,a3,s,k,e,m,v,tr.
+      step ge (State f (Sfor a1 a2 a3 lb s lp) k e m)
+           E0 (State f a1 (Kseq (Sfor Sskip a2 a3 lb s lp) k) e m)
+  | step_for_false: ∀f,a2,a3,lb,s,lp,k,e,m,v,tr.
       eval_expr ge e m a2 v tr →
       is_false v (typeof a2) →
-      step ge (State f (Sfor Sskip a2 a3 s) k e m)
-           tr (State f Sskip k e m)
-  | step_for_true: ∀f,a2,a3,s,k,e,m,v,tr.
+      step ge (State f (Sfor Sskip a2 a3 lb s lp) k e m)
+           tr (State f (optional_cost lp Sskip) k e m)
+  | step_for_true: ∀f,a2,a3,lb,s,lp,k,e,m,v,tr.
       eval_expr ge e m a2 v tr →
       is_true v (typeof a2) →
-      step ge (State f (Sfor Sskip a2 a3 s) k e m)
-           tr (State f s (Kfor2 a2 a3 s k) e m)
-  | step_skip_or_continue_for2: ∀f,x,a2,a3,s,k,e,m.
+      step ge (State f (Sfor Sskip a2 a3 lb s lp) k e m)
+           tr (State f (optional_cost lb s) (Kfor2 a2 a3 lb s lp k) e m)
+  | step_skip_or_continue_for2: ∀f,x,a2,a3,lb,s,lp,k,e,m.
       x = Sskip ∨ x = Scontinue →
-      step ge (State f x (Kfor2 a2 a3 s k) e m)
-           E0 (State f a3 (Kfor3 a2 a3 s k) e m)
-  | step_break_for2: ∀f,a2,a3,s,k,e,m.
-      step ge (State f Sbreak (Kfor2 a2 a3 s k) e m)
-           E0 (State f Sskip k e m)
-  | step_skip_for3: ∀f,a2,a3,s,k,e,m.
-      step ge (State f Sskip (Kfor3 a2 a3 s k) e m)
-           E0 (State f (Sfor Sskip a2 a3 s) k e m)
+      step ge (State f x (Kfor2 a2 a3 lb s lp k) e m)
+           E0 (State f a3 (Kfor3 a2 a3 lb s lp k) e m)
+  | step_break_for2: ∀f,a2,a3,lb,s,lp,k,e,m.
+      step ge (State f Sbreak (Kfor2 a2 a3 lb s lp k) e m)
+           E0 (State f (optional_cost lp Sskip) k e m)
+  | step_skip_for3: ∀f,a2,a3,lb,s,lp,k,e,m.
+      step ge (State f Sskip (Kfor3 a2 a3 lb s lp k) e m)
+           E0 (State f (Sfor Sskip a2 a3 lb s lp) k e m)
 
   | step_return_0: ∀f,k,e,m.
       fn_return f = Tvoid →

src/Clight/Csyntax.ma

@@ -183 +183 @@
 (* * Clight statements include all C statements.
   Only structured forms of [switch] are supported; moreover,
   the [default] case must occur last.  Blocks and block-scoped declarations
-  are not supported. *)
+  are not supported.
+  
+  The loops have optional cost labels for the body of the loop and for after
+  the loop is complete (usually denoted lb and lp respectively in definitions).
+  By closely associating the cost labels with the syntax it is easier to write
+  the code to compile loops without introducing extraneous statements between
+  control flow and cost labels.
+   *)
 
 definition label ≝ ident.
 
@@ -193 +200 @@
   | Scall: option expr → expr → list expr → statement (**r function call *)
   | Ssequence : statement → statement → statement  (**r sequence *)
   | Sifthenelse : expr  → statement → statement → statement (**r conditional *)
-  | Swhile : expr → statement → option costlabel → statement   (**r [while] loop *)
-  | Sdowhile : expr → statement → statement (**r [do] loop *)
-  | Sfor: statement → expr → statement → statement → statement (**r [for] loop *)
+  | Swhile : expr → option costlabel → statement → option costlabel → statement   (**r [while] loop *)
+  | Sdowhile : expr → option costlabel → statement → option costlabel → statement (**r [do] loop *)
+  | Sfor: statement → expr → statement → option costlabel → statement → option costlabel → statement (**r [for] loop *)
   | Sbreak : statement                      (**r [break] statement *)
   | Scontinue : statement                   (**r [continue] statement *)
   | Sreturn : option expr → statement       (**r [return] statement *)
@@ -225 +232 @@
   (Sca:∀eo,e,args. P (Scall eo e args))
   (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
   (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
-  (Swh:∀e,s,l. P s → P (Swhile e s l))
-  (Sdo:∀e,s. P s → P (Sdowhile e s))
-  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
+  (Swh:∀e,s,lb,lp. P s → P (Swhile e lb s lp))
+  (Sdo:∀e,s,lb,lp. P s → P (Sdowhile e lb s lp))
+  (Sfo:∀s1,e,s2,s3,lb,lp. P s1 → P s2 → P s3 → P (Sfor s1 e s2 lb s3 lp))
   (Sbr:P Sbreak)
   (Sco:P Scontinue)
   (Sre:∀eo. P (Sreturn eo))
@@ -248 +255 @@
 | Sifthenelse e s1 s2 ⇒ Sif e s1 s2
     (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
     (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
-| Swhile e s cl ⇒ Swh e s cl
+| Swhile e lb s lp ⇒ Swh e s lb lp
     (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
-| Sdowhile e s ⇒ Sdo e s
+| Sdowhile e lb s lp ⇒ Sdo e s lb lp
     (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
-| Sfor s1 e s2 s3 ⇒ Sfo s1 e s2 s3
+| Sfor s1 e s2 lb s3 lp ⇒ Sfo s1 e s2 s3 lb lp
     (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
     (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
     (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s3)
@@ -274 +281 @@
   (Sca:∀eo,e,args. P (Scall eo e args))
   (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
   (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
-  (Swh:∀e,s,l. P s → P (Swhile e s l))
-  (Sdo:∀e,s. P s → P (Sdowhile e s))
-  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
+  (Swh:∀e,s,lb,lp. P s → P (Swhile e lb s lp))
+  (Sdo:∀e,s,lb,lp. P s → P (Sdowhile e lb s lp))
+  (Sfo:∀s1,e,s2,s3,lb,lp. P s1 → P s2 → P s3 → P (Sfor s1 e s2 lb s3 lp))
   (Sbr:P Sbreak)
   (Sco:P Scontinue)
   (Sre:∀eo. P (Sreturn eo))

src/Clight/SimplifyCasts.ma

@@ -1981 +1981 @@
 | Scall eo e es ⇒ Scall (option_map ?? simplify_e eo) (simplify_e e) (map ?? simplify_e es)
 | Ssequence s1 s2 ⇒ Ssequence (simplify_statement s1) (simplify_statement s2)
 | Sifthenelse e s1 s2 ⇒ Sifthenelse (simplify_e e) (simplify_statement s1) (simplify_statement s2) (* TODO: try to reduce size of e *)
-| Swhile e s1 cl ⇒ Swhile (simplify_e e) (simplify_statement s1) cl (* TODO: try to reduce size of e *)
-| Sdowhile e s1 ⇒ Sdowhile (simplify_e e) (simplify_statement s1) (* TODO: try to reduce size of e *)
-| Sfor s1 e s2 s3 ⇒ Sfor (simplify_statement s1) (simplify_e e) (simplify_statement s2) (simplify_statement s3) (* TODO: reduce size of e *)
+| Swhile e lb s1 lp ⇒ Swhile (simplify_e e) lb (simplify_statement s1) lp (* TODO: try to reduce size of e *)
+| Sdowhile e lb s1 lp ⇒ Sdowhile (simplify_e e) lb (simplify_statement s1) lp (* TODO: try to reduce size of e *)
+| Sfor s1 e s2 lb s3 lp ⇒ Sfor (simplify_statement s1) (simplify_e e) (simplify_statement s2) lb (simplify_statement s3) lp (* TODO: reduce size of e *)
 | Sbreak ⇒ Sbreak
 | Scontinue ⇒ Scontinue
 | Sreturn eo ⇒ Sreturn (option_map ?? simplify_e eo)
@@ -2014 +2014 @@
 inductive cont_cast : cont → cont → Prop ≝
 | cc_stop : cont_cast Kstop Kstop
 | cc_seq : ∀s,k,k'. cont_cast k k' → cont_cast (Kseq s k) (Kseq (simplify_statement s) k')
-| cc_while : ∀e,s,cl,k,k'.
+| cc_while : ∀e,lb,s,lp,k,k'.
     cont_cast k k' →
-    cont_cast (Kwhile e s cl k) (Kwhile (simplify_e e) (simplify_statement s) cl k')
-| cc_dowhile : ∀e,s,k,k'.
+    cont_cast (Kwhile e lb s lp k) (Kwhile (simplify_e e) lb (simplify_statement s) lp k')
+| cc_dowhile : ∀e,lb,s,lp,k,k'.
     cont_cast k k' →
-    cont_cast (Kdowhile e s k) (Kdowhile (simplify_e e) (simplify_statement s) k')
-| cc_for1 : ∀e,s1,s2,k,k'.
+    cont_cast (Kdowhile e lb s lp k) (Kdowhile (simplify_e e) lb (simplify_statement s) lp k')
+| cc_for1 : ∀e,s1,lb,s2,lp,k,k'.
     cont_cast k k' →
-    cont_cast (Kseq (Sfor Sskip e s1 s2) k) (Kseq (Sfor Sskip (simplify_e e) (simplify_statement s1) (simplify_statement s2)) k')
-| cc_for2 : ∀e,s1,s2,k,k'. 
+    cont_cast (Kseq (Sfor Sskip e s1 lb s2 lp) k) (Kseq (Sfor Sskip (simplify_e e) (simplify_statement s1) lb (simplify_statement s2) lp) k')
+| cc_for2 : ∀e,s1,lb,s2,lp,k,k'. 
     cont_cast k k' →
-    cont_cast (Kfor2 e s1 s2 k) (Kfor2 (simplify_e e) (simplify_statement s1) (simplify_statement s2) k')
-| cc_for3 : ∀e,s1,s2,k,k'. 
+    cont_cast (Kfor2 e s1 lb s2 lp k) (Kfor2 (simplify_e e) (simplify_statement s1) lb (simplify_statement s2) lp k')
+| cc_for3 : ∀e,s1,lb,s2,lp,k,k'. 
     cont_cast k k' → 
-    cont_cast (Kfor3 e s1 s2 k) (Kfor3 (simplify_e e) (simplify_statement s1) (simplify_statement s2) k')
+    cont_cast (Kfor3 e s1 lb s2 lp k) (Kfor3 (simplify_e e) (simplify_statement s1) lb (simplify_statement s2) lp k')
 | cc_switch : ∀k,k'. 
     cont_cast k k' → cont_cast (Kswitch k) (Kswitch k')
 | cc_call : ∀r,f,en,k,k'. 
@@ -2423 +2423 @@
                normalize nodelta %{kst'} /2/
           | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta //
      ] ]
-| 6: #e #s #cl #Hind_s #k #k' #Hcont_cast
+| 6: #e #s #lb #lp #Hind_s #k #k' #Hcont_cast
      whd in match (find_label ???);
      whd in match (find_label ? (simplify_statement ?) ?);
-     elim (elim_IH_aux lab s (Kwhile e s cl k) (Kwhile (simplify_e e) (simplify_statement s) cl k') ? Hind_s)
+     elim (elim_IH_aux lab s (Kwhile e lb s lp k) (Kwhile (simplify_e e) lb (simplify_statement s) lp k') ? Hind_s)
      [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
           normalize nodelta %{kst'} /2/
      | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta //
      | 3: @cc_while // ]
-| 7: #e #s #Hind_s #k #k' #Hcont_cast
+| 7: #e #s #lb #lp #Hind_s #k #k' #Hcont_cast
      whd in match (find_label ???);
      whd in match (find_label ? (simplify_statement ?) ?);
-     elim (elim_IH_aux lab s (Kdowhile e s k) (Kdowhile (simplify_e e) (simplify_statement s) k') ? Hind_s)
+     elim (elim_IH_aux lab s (Kdowhile e lb s lp k) (Kdowhile (simplify_e e) lb (simplify_statement s) lp k') ? Hind_s)
      [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
           normalize nodelta %{kst'} /2/
      | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta //
      | 3: @cc_dowhile // ]
-| 8: #s1 #cond #s2 #s3 #Hind_s1 #Hind_s2 #Hind_s3 #k #k' #Hcont_cast     
+| 8: #s1 #cond #s2 #s3 #lb #lp #Hind_s1 #Hind_s2 #Hind_s3 #k #k' #Hcont_cast     
      whd in match (find_label ???);
      whd in match (find_label ? (simplify_statement ?) ?);
      elim (elim_IH_aux lab s1
-               (Kseq (Sfor Sskip cond s2 s3) k)
-               (Kseq (Sfor Sskip (simplify_e cond) (simplify_statement s2) (simplify_statement s3)) k')
+               (Kseq (Sfor Sskip cond s2 lb s3 lp) k)
+               (Kseq (Sfor Sskip (simplify_e cond) (simplify_statement s2) lb (simplify_statement s3) lp) k')
                ? Hind_s1)
      [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
           normalize nodelta %{kst'} /2/
      | 3: @cc_for1 //
      | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta
           elim (elim_IH_aux lab s3
-                    (Kfor2 cond s2 s3 k)
-                    (Kfor2 (simplify_e cond) (simplify_statement s2) (simplify_statement s3) k')
+                    (Kfor2 cond s2 lb s3 lp k)
+                    (Kfor2 (simplify_e cond) (simplify_statement s2) lb (simplify_statement s3) lp k')
                       ? Hind_s3)
           [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
                 normalize nodelta %{kst'} /2/
           | 3: @cc_for2 //
           | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta
                elim (elim_IH_aux lab s2
-                         (Kfor3 cond s2 s3 k)
-                         (Kfor3 (simplify_e cond) (simplify_statement s2) (simplify_statement s3) k')
+                         (Kfor3 cond s2 lb s3 lp k)
+                         (Kfor3 (simplify_e cond) (simplify_statement s2) lb (simplify_statement s3) lp k')
                            ? Hind_s2)
                [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
                     normalize nodelta %{kst'} /2/
@@ -2590 +2590 @@
      lapply (related_globals_lvalue_simulation ge ge' en m Hrelated) #Hsim_lvalue_related
      cases stm
      (* Perform the intros for the statements*)
-     [ 1: | 2: #lhs #rhs | 3: #ret #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #body
-     | 7: #cond #body | 8: #init #cond #step #body | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body
+     [ 1: | 2: #lhs #rhs | 3: #ret #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #lb #body #lp
+     | 7: #cond #lb #body #lp | 8: #init #cond #step #lb #body #lp | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body
      | 14: #lab | 15: #cost #body ]
      [ 1: (* Skip *)
           #Heq_s1 #Heq_s1' #_ lapply Houtcome >Heq_s1
@@ -2615 +2615 @@
                %{(State (simplify_function f) (simplify_statement stm') k0' en m)} @conj
                [ 1: // | 2: %1 // ]               
           | 3: (* Kwhile *)
-               #cond #body #cl #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq
+               #cond #lb #body #lp #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq
                whd in match (ret ??) in Eq; destruct (Eq)               
-               %{(State (simplify_function f) (Swhile (simplify_e cond) (simplify_statement body) cl) k0' en m)} @conj
+               %{(State (simplify_function f) (Swhile (simplify_e cond) lb (simplify_statement body) lp) k0' en m)} @conj
                [ 1: // | 2: %1 // ]
           | 4: (* Kdowhile *)
-               #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq
+               #cond #lb #body #lp #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq
                elim (Hsim_related cond) #Hsim_cond #Htype_cond_eq cases Hsim_cond
                [ 2: * #error #Hfail >Hfail in Eq; #Habsurd normalize in Habsurd; destruct
                | 1: cases (exec_expr ge en m cond) in Eq;
@@ -2635 +2635 @@
                          | 1: * whd in match (bindIO ??????); 
                                 whd in match (bindIO ??????);
                                 #Eq destruct (Eq)
-                              [ 1: %{(State (simplify_function f) (Sdowhile (simplify_e cond) (simplify_statement body)) k0' en m)}
-                                   @conj [ 1: // | 2: %1 // ]
-                              | 2: %{(State (simplify_function f) Sskip k0' en m)}
+                              [ 1: %{(State (simplify_function f) (Sdowhile (simplify_e cond) lb (simplify_statement body) lp) k0' en m)}
                                    @conj [ 1: // | 2: %1 // ]
+                              | 2: %{(State (simplify_function f) (optional_cost lp Sskip) k0' en m)}
+                                   @conj [ 1: // | 2: cases lp [2:#lp'] %1 // ]
                               ]
                          ]
                     ]
                ]
            | 5,6,7:
-                #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq
+                #cond #step #lb #body #lp #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq
                 whd in match (ret ??) in Eq ⊢ %; destruct (Eq)
                 [ 1: %{(State (simplify_function f) 
-                              (Sfor Sskip (simplify_e cond) (simplify_statement step) (simplify_statement body)) 
+                              (Sfor Sskip (simplify_e cond) (simplify_statement step) lb (simplify_statement body) lp) 
                                k0' en m)} @conj
                      [ 1: // | 2: %1 // ]
                 | 2: %{(State (simplify_function f) 
                               (simplify_statement step) 
-                              (Kfor3 (simplify_e cond) (simplify_statement step) (simplify_statement body) k0')
+                              (Kfor3 (simplify_e cond) (simplify_statement step) lb (simplify_statement body) lp k0')
                               en m)} @conj
                      [ 1: // | 2: %1 @cc_for3 // ]
                 | 3: %{(State (simplify_function f)
                               (Sfor Sskip (simplify_e cond) (simplify_statement step)
-                              (simplify_statement body)) 
+                              lb (simplify_statement body) lp) 
                               k0' en m)} @conj
                      [ 1: // | 2: %1 // ]
                 ]
@@ -2782 +2782 @@
                              %{(State (simplify_function f) (simplify_statement iffalse) k' en m)} @conj
                              [ 1: // | 2: <e0 %1 // ]
                         ] ] ] ]
-    | 6: #cl #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; 
+    | 6: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; 
          whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
          whd in match (exec_step ??) in Heq ⊢ %;
          elim (Hsim_related cond) in Heq; *
@@ -2797 +2797 @@
                    [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
                    | 1: * whd in match (bindIO ??????) in ⊢ (% → %); #Heq normalize nodelta in Heq ⊢ %;
                         [ 1: destruct skip (condtrace)
-                             %{(State (simplify_function f) (simplify_statement body) (Kwhile (simplify_e cond) (simplify_statement body) cl k') en m)}
+                             %{(State (simplify_function f) (optional_cost lb (simplify_statement body)) (Kwhile (simplify_e cond) lb (simplify_statement body) lp k') en m)}
                              @conj
-                             [ 1: // | 2: <e0 %1 @cc_while // ]
+                             [ 1: // | 2: <e0 cases lb [2: #lb'] %1 @cc_while // ]
                         | 2: destruct skip (condtrace)
-                             %{(State (simplify_function f) (optional_cost cl Sskip) k' en m)} @conj
-                             [ 1: // | 2: <e0 cases cl [2:#cl'] %1 // ]
+                             %{(State (simplify_function f) (optional_cost lp Sskip) k' en m)} @conj
+                             [ 1: // | 2: <e0 cases lp [2:#lp'] %1 // ]
                         ] ] ] ]
     | 7: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
          whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
          whd in match (exec_step ??) in Heq ⊢ %;
          destruct (Heq)
-         %{(State (simplify_function f) (simplify_statement body)
-                  (Kdowhile (simplify_e cond) (simplify_statement body) k') en m)} @conj
-         [ 1: // | 2: %1 @cc_dowhile // ]
+         %{(State (simplify_function f) (optional_cost lb (simplify_statement body))
+                  (Kdowhile (simplify_e cond) lb (simplify_statement body) lp k') en m)} @conj
+         [ 1: // | 2: cases lb [2:#lb'] %1 @cc_dowhile // ]
     | 8: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
          whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
          whd in match (exec_step ??) in Heq ⊢ %;
@@ -2820 +2820 @@
               whd in match (ret ??) in ⊢ (% → %);
               #Eq destruct (Eq)
               %{(State (simplify_function f) (simplify_statement init)
-                       (Kseq (Sfor Sskip (simplify_e cond) (simplify_statement step) (simplify_statement body)) k') en m)} @conj
+                       (Kseq (Sfor Sskip (simplify_e cond) (simplify_statement step) lb (simplify_statement body) lp) k') en m)} @conj
               [ 1: // | 2: %1 @cc_for1 // ]   
          | 1: #Hinit_eq_Sskip >Hinit_eq_Sskip 
               whd in match (simplify_statement ?);
@@ -2837 +2837 @@
                         [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
                         | 1: * whd in match (bindIO ??????); whd in match (bindIO ??????);
                              normalize nodelta #Heq destruct (Heq)
-                             [ 1: %{(State (simplify_function f) (simplify_statement body)
-                                           (Kfor2 (simplify_e cond) (simplify_statement step) (simplify_statement body) k') en m)}
-                                   @conj [ 1: // | 2: %1 @cc_for2 // ]
-                             | 2: %{(State (simplify_function f) Sskip k' en m)} @conj
-                                  [ 1: // | 2: %1 // ]
+                             [ 1: %{(State (simplify_function f) (optional_cost lb (simplify_statement body))
+                                           (Kfor2 (simplify_e cond) (simplify_statement step) lb (simplify_statement body) lp k') en m)}
+                                   @conj [ 1: // | 2: cases lb [2:#lb'] %1 @cc_for2 // ]
+                             | 2: %{(State (simplify_function f) (optional_cost lp Sskip) k' en m)} @conj
+                                  [ 1: // | 2: cases lp [2:#lp'] %1 // ]
          ] ] ] ] ]
     | 9: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
          whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
@@ -2849 +2849 @@
          inversion Hcont_cast in Heq; normalize nodelta
          [ 1: #Hk #Hk' #_
          | 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ 
-         | 3: #cond #body #cl #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
-         | 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
-         | 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ 
+         | 3: #cond #lb #body #lp #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
+         | 4: #cond #lb #body #lp #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
+         | 5,6,7: #cond #step #lb #body #lp #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ 
          | 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
          | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ ]
          #H whd in match (ret ??) in H ⊢ %;
          destruct (H)
          [ 1,4: %{(State (simplify_function f) Sbreak k0' en m)} @conj [ 1,3: // | 2,4: %1 // ]
-         | %{(State (simplify_function f) (optional_cost cl Sskip) k0' en m)} @conj try // cases cl [2:#cl'] %1 //
-         | 3,5,6: %{(State (simplify_function f) Sskip k0' en m)} @conj try // %1 // ]
+         | 2,3,5: %{(State (simplify_function f) (optional_cost lp Sskip) k0' en m)} @conj try // cases lp [2,4,6:#lp'] %1 //
+         | 6: %{(State (simplify_function f) Sskip k0' en m)} @conj try // %1 // ]
     | 10: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
          whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
          whd in match (exec_step ??) in Heq ⊢ %;
          inversion Hcont_cast in Heq; normalize nodelta
          [ 1: #Hk #Hk' #_
          | 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ 
-         | 3: #cond #body #cl #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
-         | 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
-         | 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ 
+         | 3: #cond #lb #body #lp #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
+         | 4: #cond #lb #body #lp #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
+         | 5,6,7: #cond #step #lb #body #lp #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ 
          | 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
          | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ ]
          #H whd in match (ret ??) in H ⊢ %;
          destruct (H)
          [ 1,4,6: %{(State (simplify_function f) Scontinue k0' en m)} @conj try // %1 //
-         | 2: %{(State (simplify_function f) (Swhile (simplify_e cond) (simplify_statement body) cl) k0' en m)} 
+         | 2: %{(State (simplify_function f) (Swhile (simplify_e cond) lb (simplify_statement body) lp) k0' en m)} 
               @conj try // %1 //
          | 3: elim (Hsim_related cond) #Hsim_cond #Htype_cond_eq elim Hsim_cond in H;
               [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
@@ -2886 +2886 @@
                         [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
                         | 1: * whd in match (bindIO ??????); whd in match (bindIO ??????);
                              normalize nodelta #Heq destruct (Heq)
-                             [ 1: %{(State (simplify_function f) (Sdowhile (simplify_e cond) (simplify_statement body)) k0' en m)}
-                                  @conj [ 1: // | 2: %1 // ]
-                             | 2: %{(State (simplify_function f) Sskip k0' en m)}
+                             [ 1: %{(State (simplify_function f) (Sdowhile (simplify_e cond) lb (simplify_statement body) lp) k0' en m)}
                                   @conj [ 1: // | 2: %1 // ]
+                             | 2: %{(State (simplify_function f) (optional_cost lp Sskip) k0' en m)}
+                                  @conj [ 1: // | 2: cases lp [2:#lp'] %1 // ]
              ] ] ] ]
          | 5: %{(State (simplify_function f) (simplify_statement step)
-                       (Kfor3 (simplify_e cond) (simplify_statement step) (simplify_statement body) k0') en m)} @conj
+                       (Kfor3 (simplify_e cond) (simplify_statement step) lb (simplify_statement body) lp k0') en m)} @conj
               [ 1: // | 2: %1 @cc_for3 // ]
          ]
     | 11: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
@@ -3007 +3007 @@
      inversion Hcont_cast 
      [ 1: #Hk #Hk' #_
      | 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ 
-     | 3: #cond #body #cl #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
-     | 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
-     | 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ 
+     | 3: #cond #lb #body #lp #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
+     | 4: #cond #lb #body #lp #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
+     | 5,6,7: #cond #step #lb #body #lp #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ 
      | 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
      | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ ]
      normalize nodelta

src/Clight/addRuntime.ma

@@ -80 +80 @@
                    match oe with [ Some e ⇒ expr_ops e @ l | None ⇒ l ]
 | Ssequence s1 s2 ⇒ stmt_ops s1 @ stmt_ops s2
 | Sifthenelse e1 s1 s2 ⇒ expr_ops e1 @ stmt_ops s1 @ stmt_ops s2
-| Swhile e1 s1   ⇒ expr_ops e1 @ stmt_ops s1
-| Sdowhile e1 s1 ⇒ expr_ops e1 @ stmt_ops s1
-| Sfor s1 e1 s2 s3 ⇒ expr_ops e1 @ stmt_ops s1 @ stmt_ops s2 @ stmt_ops s3
+| Swhile e1 _ s1 _ ⇒ expr_ops e1 @ stmt_ops s1
+| Sdowhile e1 _ s1 _ ⇒ expr_ops e1 @ stmt_ops s1
+| Sfor s1 e1 s2 _ s3 _ ⇒ expr_ops e1 @ stmt_ops s1 @ stmt_ops s2 @ stmt_ops s3
 | Sreturn oe ⇒ match oe with [ Some e ⇒ expr_ops e | None ⇒ [ ] ]
 | Sswitch e1 ls ⇒ expr_ops e1 @ lstmt_ops ls
 | Slabel _ s1 ⇒ stmt_ops s1
@@ -210 +210 @@
 
   (* This is particularly bad - for loops we end up duplicating the code. *)
   
-| Swhile e1 s1 ⇒
+| Swhile e1 lb s1 lp ⇒
     let 〈ls1,e1,u〉 ≝ subst_expr e1 rs u in
     let 〈s1,u〉 ≝ subst_stmt s1 rs u in
-      〈rev_prepend_stmts ls1 (Swhile e1 (append_stmts s1 ls1)), u〉
-| Sdowhile e1 s1 ⇒
+      〈rev_prepend_stmts ls1 (Swhile e1 lb (append_stmts s1 ls1) lp), u〉
+| Sdowhile e1 lb s1 lp ⇒
     let 〈ls1,e1,u〉 ≝ subst_expr e1 rs u in
     let 〈s1,u〉 ≝ subst_stmt s1 rs u in
-      〈Sdowhile e1 (append_stmts s1 ls1), u〉
-| Sfor s1 e1 s2 s3 ⇒
+      〈Sdowhile e1 lb (append_stmts s1 ls1) lp, u〉
+| Sfor s1 e1 s2 lb s3 lp ⇒
     let 〈ls1,e1,u〉 ≝ subst_expr e1 rs u in
     let 〈s1,u〉 ≝ subst_stmt s1 rs u in
     let 〈s2,u〉 ≝ subst_stmt s2 rs u in
     let 〈s3,u〉 ≝ subst_stmt s3 rs u in
-      〈Sfor (append_stmts s1 ls1) e1 s2 (append_stmts s3 ls1), u〉
+      〈Sfor (append_stmts s1 ls1) e1 s2 lb (append_stmts s3 ls1) lp, u〉
 | Sreturn oe ⇒
     match oe with
     [ Some e ⇒ let 〈ls1,e,u〉 ≝ subst_expr e rs u in 〈rev_prepend_stmts ls1 (Sreturn (Some ? e)), u〉
@@ -291 +291 @@
       (Ssequence
         (Swhile
           (Expr (Ebinop Oge (Expr (Evar x) uint) (Expr (Evar y) uint)) uint)
+          (None ?)
           (Ssequence
             (Sassign (Expr (Evar x) uint) (Expr (Ebinop Osub (Expr (Evar x) uint) (Expr (Evar y) uint)) uint))
-            (Sassign (Expr (Evar quo) uint) (Expr (Ebinop Oadd (Expr (Evar quo) uint) (Expr (Econst_int sz (repr sz 1)) uint)) uint))))
+            (Sassign (Expr (Evar quo) uint) (Expr (Ebinop Oadd (Expr (Evar quo) uint) (Expr (Econst_int sz (repr sz 1)) uint)) uint)))
+          (None ?) )
         (Sreturn (Some ? (Expr (Evar quo) uint))))))),
     u〉.
         

src/Clight/label.ma

@@ -20 +20 @@
   ]
 ].
 
+definition is_none : ∀A:Type[0]. option A → bool ≝
+λA,o. match o with [ None ⇒ true | Some _ ⇒ false ].
+
 let rec statement_label_free (s:statement) : bool ≝
 match s with
 [ Sassign e1 e2 ⇒ expr_label_free e1 ∧ expr_label_free e2
 | Scall oe e1 es ⇒ option_map_def … expr_label_free true oe ∧ expr_label_free e1 ∧ all … expr_label_free es
 | Ssequence s1 s2 ⇒ statement_label_free s1 ∧ statement_label_free s2
 | Sifthenelse e1 s1 s2 ⇒ expr_label_free e1 ∧ statement_label_free s1 ∧ statement_label_free s2
-| Swhile e1 s1 cl ⇒ expr_label_free e1 ∧ statement_label_free s1 ∧ match cl with [ None ⇒ true | _ ⇒ false ]
-| Sdowhile e1 s1 ⇒ expr_label_free e1 ∧ statement_label_free s1
-| Sfor s1 e1 s2 s3 ⇒ statement_label_free s1 ∧ expr_label_free e1 ∧ statement_label_free s2 ∧ statement_label_free s3
+| Swhile e1 lb s1 lp ⇒ expr_label_free e1 ∧ statement_label_free s1 ∧ is_none … lb ∧ is_none … lp
+| Sdowhile e1 lb s1 lp ⇒ expr_label_free e1 ∧ statement_label_free s1 ∧ is_none … lb ∧ is_none … lp
+| Sfor s1 e1 s2 lb s3 lp ⇒ statement_label_free s1 ∧ expr_label_free e1 ∧ statement_label_free s2 ∧ statement_label_free s3 ∧ is_none … lb ∧ is_none … lp
 | Sreturn oe ⇒ option_map_def … expr_label_free true oe
 | Sswitch e1 ls ⇒ expr_label_free e1 ∧ labeled_statements_label_free ls
 | Slabel _ s1 ⇒ statement_label_free s1
@@ -177 +180 @@
     let 〈s2,costgen〉 ≝ label_statement s2 costgen in
     let 〈s2,costgen〉 ≝ add_cost_before s2 costgen in
     〈Sifthenelse e s1 s2, costgen〉
-| Swhile e s' cl ⇒
+| Swhile e lb s' lp ⇒
     let 〈e,costgen〉 ≝ label_expr e costgen in 
+    let 〈body,costgen〉 ≝ ensure_label lb costgen in
     let 〈s',costgen〉 ≝ label_statement s' costgen in
-    let 〈s',costgen〉 ≝ add_cost_before s' costgen in
-    let 〈after,costgen〉 ≝ ensure_label cl costgen in
-    〈Swhile e s' (Some ? after), costgen〉
-| Sdowhile e s' ⇒
+    let 〈after,costgen〉 ≝ ensure_label lp costgen in
+    〈Swhile e (Some ? body) s' (Some ? after), costgen〉
+| Sdowhile e lb s' lp ⇒
     let 〈e,costgen〉 ≝ label_expr e costgen in 
+    let 〈body,costgen〉 ≝ ensure_label lb costgen in
     let 〈s',costgen〉 ≝ label_statement s' costgen in
-    let 〈s',costgen〉 ≝ add_cost_before s' costgen in
-    let 〈s,costgen〉 ≝ add_cost_after (Sdowhile e s') costgen in
-    〈s,costgen〉
-| Sfor s1 e s2 s3 ⇒
+    let 〈after,costgen〉 ≝ ensure_label lp costgen in
+    〈Sdowhile e (Some ? body) s' (Some ? after),costgen〉
+| Sfor s1 e s2 lb s3 lp ⇒
     let 〈e,costgen〉 ≝ label_expr e costgen in 
     let 〈s1,costgen〉 ≝ label_statement s1 costgen in
     let 〈s2,costgen〉 ≝ label_statement s2 costgen in
+    let 〈body,costgen〉 ≝ ensure_label lb costgen in
     let 〈s3,costgen〉 ≝ label_statement s3 costgen in
-    let 〈s3,costgen〉 ≝ add_cost_before s3 costgen in
-    let 〈s,costgen〉 ≝ add_cost_after (Sfor s1 e s2 s3) costgen in
-    〈s,costgen〉
+    let 〈after,costgen〉 ≝ ensure_label lp costgen in
+    〈Sfor s1 e s2 (Some ? body) s3 (Some ? after),costgen〉
 | Sbreak ⇒ 〈Sbreak,costgen〉
 | Scontinue ⇒ 〈Scontinue,costgen〉
 | Sreturn opt_e ⇒

src/Clight/labelSimulation.ma

@@ -257 +257 @@
   | /2/ ] | skip ]
 ] qed.
 
+inductive label_le : option costlabel → costlabel → Prop ≝
+| ll_none : ∀c. label_le (None ?) c
+| ll_some : ∀c. label_le (Some ? c) c.
 
 (* Now we move on to describe the simulation relation.  First, relate the
    continuations. *)
 inductive cont_with_labels : cont → cont → Prop ≝
 | cwl_stop : cont_with_labels Kstop Kstop
 | cwl_seq : ∀u,s,k,k'. cont_with_labels k k' → cont_with_labels (Kseq s k) (Kseq (\fst (label_statement s u)) k')
-| cwl_while : ∀ue,e,us,s,cl,cs,cpost,k,k'.
+| cwl_while : ∀ue,e,us,lb,s,lp,cs,cpost,k,k'.
     cont_with_labels k k' →
-    (cl = None ? ∨ cl = Some ? cpost) →
-    cont_with_labels (Kwhile e s cl k) (Kwhile (\fst (label_expr e ue)) (Scost cs (\fst (label_statement s us))) (Some ? cpost) k')
-| cwl_dowhile : ∀ue,e,us,s,cs,cpost,k,k'.
+    label_le lb cs →
+    label_le lp cpost →
+    cont_with_labels (Kwhile e lb s lp k) (Kwhile (\fst (label_expr e ue)) (Some ? cs) (\fst (label_statement s us)) (Some ? cpost) k')
+| cwl_dowhile : ∀ue,e,us,lb,s,lp,cs,cpost,k,k'.
     cont_with_labels k k' →
-    cont_with_labels (Kdowhile e s k) (Kdowhile (\fst (label_expr e ue)) (Scost cs (\fst (label_statement s us))) (Kseq (Scost cpost Sskip) k'))
-| cwl_for1 : ∀ue,e,us1,s1,us2,s2,cs,cpost,k,k'.
+    label_le lb cs →
+    label_le lp cpost →
+    cont_with_labels (Kdowhile e lb s lp k) (Kdowhile (\fst (label_expr e ue)) (Some ? cs) (\fst (label_statement s us)) (Some ? cpost) k')
+| cwl_for1 : ∀ue,e,us1,s1,us2,lb,s2,lp,cs,cpost,k,k'.
     cont_with_labels k k' →
-    cont_with_labels (Kseq (Sfor Sskip e s1 s2) k) (Kseq (Sfor Sskip (\fst (label_expr e ue)) (\fst (label_statement s1 us1)) (Scost cs (\fst (label_statement s2 us2)))) (Kseq (Scost cpost Sskip) k'))
-| cwl_for2 : ∀ue,e,us1,s1,us2,s2,cs,cpost,k,k'. cont_with_labels k k' → cont_with_labels (Kfor2 e s1 s2 k) (Kfor2 (\fst (label_expr e ue)) (\fst (label_statement s1 us1)) (Scost cs (\fst (label_statement s2 us2))) (Kseq (Scost cpost Sskip) k'))
-| cwl_for3 : ∀ue,e,us1,s1,us2,s2,cs,cpost,k,k'. cont_with_labels k k' → cont_with_labels (Kfor3 e s1 s2 k) (Kfor3 (\fst (label_expr e ue)) (\fst (label_statement s1 us1)) (Scost cs (\fst (label_statement s2 us2))) (Kseq (Scost cpost Sskip) k'))
+    label_le lb cs →
+    label_le lp cpost →
+    cont_with_labels (Kseq (Sfor Sskip e s1 lb s2 lp) k) (Kseq (Sfor Sskip (\fst (label_expr e ue)) (\fst (label_statement s1 us1)) (Some ? cs) (\fst (label_statement s2 us2)) (Some ? cpost)) k')
+| cwl_for2 : ∀ue,e,us1,s1,us2,lb,s2,lp,cs,cpost,k,k'.
+    cont_with_labels k k' →
+    label_le lb cs →
+    label_le lp cpost →
+    cont_with_labels (Kfor2 e s1 lb s2 lp k) (Kfor2 (\fst (label_expr e ue)) (\fst (label_statement s1 us1)) (Some ? cs) (\fst (label_statement s2 us2)) (Some ? cpost) k')
+| cwl_for3 : ∀ue,e,us1,s1,us2,lb,s2,lp,cs,cpost,k,k'.
+    cont_with_labels k k' →
+    label_le lb cs →
+    label_le lp cpost →
+    cont_with_labels (Kfor3 e s1 lb s2 lp k) (Kfor3 (\fst (label_expr e ue)) (\fst (label_statement s1 us1)) (Some ? cs) (\fst (label_statement s2 us2)) (Some ? cpost) k')
 | cwl_switch : ∀k,k'. cont_with_labels k k' → cont_with_labels (Kswitch k) (Kswitch k')
 | cwl_call : ∀g,r,f,en,k,k'. cont_with_labels k k' → cont_with_labels (Kcall r f en k) (Kcall r (\fst (label_function g f)) en k')
 | cwl_seqls : ∀ls,u,k,k'. cont_with_labels k k' →
@@ -290 +306 @@
 inductive state_with_labels_partial : state → state → Prop ≝
 | swl_state : ∀g,f,us,s,k,k',e,m. cont_with_labels k k' → state_with_labels_partial (State f s k e m) (State (\fst (label_function g f)) (\fst (label_statement s us)) k' e m)
 (* Extra matching states that we can reach that don't quite correspond to the
-   labelling function *)
-| swl_whilestate : ∀g,f,ua,a,us,s,cl,cs,cpost,k,k',e,m. cont_with_labels k k' →
-    (cl = None ? ∨ cl = Some ? cpost) →
-    state_with_labels_partial (State f (Swhile a s cl) k e m) (State (\fst (label_function g f)) (Swhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us))) (Some ? cpost)) k' e m)
-| swl_dowhilestate : ∀g,f,ua,a,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' →
-    state_with_labels_partial (State f (Sdowhile a s) k e m) (State (\fst (label_function g f)) (Sdowhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
-| swl_forstate : ∀g,f,ua2,a2,us3,s3,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' →
-    state_with_labels_partial (State f (Sfor Sskip a2 s3 s) k e m) (State (\fst (label_function g f)) (Sfor Sskip (\fst (label_expr a2 ua2)) (\fst (label_statement s3 us3)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
+   labelling function because we've forgotten the relationship between the
+   fresh labels *)
+| swl_whilestate : ∀g,f,ua,a,us,lb,s,lp,cs,cpost,k,k',e,m. cont_with_labels k k' →
+    label_le lb cs →
+    label_le lp cpost →
+    state_with_labels_partial (State f (Swhile a lb s lp) k e m) (State (\fst (label_function g f)) (Swhile (\fst (label_expr a ua)) (Some ? cs) (\fst (label_statement s us)) (Some ? cpost)) k' e m)
+| swl_dowhilestate : ∀g,f,ua,a,us,lb,s,lp,cs,cpost,k,k',e,m. cont_with_labels k k' →
+    label_le lb cs →
+    label_le lp cpost →
+    state_with_labels_partial (State f (Sdowhile a lb s lp) k e m) (State (\fst (label_function g f)) (Sdowhile (\fst (label_expr a ua)) (Some ? cs) (\fst (label_statement s us)) (Some ? cpost)) k' e m)
+| swl_forstate : ∀g,f,ua2,a2,us3,s3,us,lb,s,lp,cs,cpost,k,k',e,m. cont_with_labels k k' →
+    label_le lb cs →
+    label_le lp cpost →
+    state_with_labels_partial (State f (Sfor Sskip a2 s3 lb s lp) k e m) (State (\fst (label_function g f)) (Sfor Sskip (\fst (label_expr a2 ua2)) (\fst (label_statement s3 us3)) (Some ? cs) (\fst (label_statement s us)) (Some ? cpost)) k' e m)
 (* and the rest *)
 | swl_callstate : ∀g,fd,args,k,k',m. cont_with_labels k k' → state_with_labels_partial (Callstate fd args k m) (Callstate (\fst (label_fundef g fd)) args k' m)
 | swl_returnstate : ∀res,k,k',m. cont_with_labels k k' → state_with_labels_partial (Returnstate res k m) (Returnstate res k' m)
@@ -373 +395 @@
   (\fst (label_statement s u)) ≠ Sskip.
 * #u
 [ * #H cases (H (refl ??))
-| *: #a try #b try #c try #d try #e
+| *: #a try #b try #c try #d try #e try #f try #g
      (* Use the state-monad-like structure of the labelling function to break
         it up *)
      whd in match (label_statement ??);
      repeat @(breakup_pair ???? (λx.\fst x ≠ Sskip))
-     % #E destruct
+     % #E lapply (eq_to_jmeq ??? E) -E #E destruct
 ] qed.
 
 lemma labelled_is_not_skip : ∀s,u.
@@ -425 +447 @@
   ]
 ] qed.
 
+lemma ensure_label_elim : ∀c,u. ∀P:costlabel × (universe CostTag) → Type[0].
+  (∀c',u'. label_le c c' → P 〈c',u'〉) →
+  P (ensure_label c u).
+* /3/
+qed.
+
 (* Break up labelling function in one go for statements. *)
 lemma blindly_label : ∀u,s. ∀P:statement → Prop.
 match s with
@@ -433 +461 @@
 | Scall eo e args ⇒ ∀u1,u2,u3. P (Scall (\fst (label_opt_expr eo u1)) (\fst (label_expr e u2)) (\fst (label_exprs args u3))) 
 | Ssequence s1 s2 ⇒ ∀u1,u2. P (Ssequence (\fst (label_statement s1 u1)) (\fst (label_statement s2 u2)))
 | Sifthenelse e s1 s2 ⇒ ∀u1,u2,u3,c2,c3. P (Sifthenelse (\fst (label_expr e u1)) (Scost c2 (\fst (label_statement s1 u2))) (Scost c3 (\fst (label_statement s2 u3))))
-| Swhile e s1 cl ⇒ ∀u1,u2,cs,cpost. cl = None ? ∨ cl = Some ? cpost → P (Swhile (\fst (label_expr e u1)) (Scost cs (\fst (label_statement s1 u2))) (Some ? cpost))
-| Sdowhile e s1 ⇒ ∀u1,u2,cs,cpost. P (Ssequence (Sdowhile (\fst (label_expr e u1)) (Scost cs (\fst (label_statement s1 u2)))) (Scost cpost Sskip))
-| Sfor s1 e s2 s3 ⇒ ∀u1,u2,u3,u4,c3,c4. P (Ssequence (Sfor (\fst (label_statement s1 u1)) (\fst (label_expr e u2)) (\fst (label_statement s2 u3)) (Scost c3 (\fst (label_statement s3 u4)))) (Scost c4 Sskip))
+| Swhile e lb s1 lp ⇒ ∀u1,u2,cs,cpost.
+    label_le lb cs →
+    label_le lp cpost →
+    P (Swhile (\fst (label_expr e u1)) (Some ? cs) (\fst (label_statement s1 u2)) (Some ? cpost))
+| Sdowhile e lb s1 lp ⇒ ∀u1,u2,cs,cpost.
+    label_le lb cs →
+    label_le lp cpost →
+    P (Sdowhile (\fst (label_expr e u1)) (Some ? cs) (\fst (label_statement s1 u2)) (Some ? cpost))
+| Sfor s1 e s2 lb s3 lp ⇒ ∀u1,u2,u3,u4,c3,c4.
+    label_le lb c3 →
+    label_le lp c4 →
+    P (Sfor (\fst (label_statement s1 u1)) (\fst (label_expr e u2)) (\fst (label_statement s2 u3)) (Some ? c3) (\fst (label_statement s3 u4)) (Some ? c4))
 | Sbreak ⇒ P Sbreak
 | Scontinue ⇒ P Scontinue
 | Sreturn eo ⇒ ∀u1. P (Sreturn (\fst (label_opt_expr eo u1)))
@@ -444 +481 @@
 | Sgoto l ⇒ P (Sgoto l)
 | Scost c s1 ⇒ ∀u1. P (Scost c (\fst (label_statement s1 u1)))
 ] → P (\fst (label_statement s u)).  
-#u * // #A #B #C try #D try #E try #F whd in match (label_statement ??);
+#u * // #A #B #C try #D try #E try #F try #G try #H whd in match (label_statement ??);
 @label_gen_elim #u1 //
+[ 5,6: @ensure_label_elim #cA #uA #HA ]
 @label_gen_elim #u2 //
-[ 6: >shift_fst //
-| 3: @label_gen_elim #u3 >shift_fst >shift_fst
-     cases C in E ⊢ %; /3/
-| *: @label_gen_elim #u3 //
-     @label_gen_elim #u4
-     [ @label_gen_elim #u5 >shift_fst >shift_fst //
-     | >shift_fst >shift_fst //
-     | @label_gen_elim #u5 >shift_fst >shift_fst >shift_fst //
-     ]
+[ 6: >shift_fst // ]
+@label_gen_elim #u3 //
+[ 1,2,4: @ensure_label_elim #cB #uB #HB ]
+@label_gen_elim #u4 /2/ 
+[ @label_gen_elim #u5 @ensure_label_elim #c6 #u6 #H6 >shift_fst /2/
+| @label_gen_elim #u5 >shift_fst >shift_fst /2/
 ] qed.
 
 (* Apply induction hypothesis in label_find_label proof below while getting
@@ -532 +567 @@
       whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?);
       @refl | // ] |skip ]| skip ]| skip ]
   ]
-| #e #s0 #cl #IH #k #k' #u #K @blindly_label #u1 #u2 #cs #cpost #CL
+| #e #s0 #lb #lp #IH #k #k' #u #K @blindly_label #u1 #u2 #cs #cpost #LB #LP
   whd in match (find_label ?? k); normalize in match (find_label ?? k');
   @(lfl_IH s0 … IH) [ /2/ ]
   cases (find_label ???)
@@ -543 +578 @@
       whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?);
       @refl | // ]| skip ]| skip ]| skip ]
   ]
-| #e #s0 #IH #k #k' #u #K @blindly_label #u1 #u2 #cs #cpost
+| #e #s0 #lb #lp #IH #k #k' #u #K @blindly_label #u1 #u2 #cs #cpost #LB #LP
   whd in match (find_label ?? k); normalize in match (find_label ?? k');
   @(lfl_IH s0 … IH) [ /2/ ]
   cases (find_label ???)
@@ -554 +589 @@
       whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?);
       @refl | // ]| skip ]| skip ]| skip ]
   ]
-| #s1 #e #s2 #s3 #IH1 #IH2 #IH3 #k #k' #u #K @blindly_label #u1 #u2 #u3 #u4 #c3 #c4
+| #s1 #e #s2 #s3 #lb #lp #IH1 #IH2 #IH3 #k #k' #u #K @blindly_label #u1 #u2 #u3 #u4 #c3 #c4 #LB #LP
   whd in match (find_label ???); normalize in match (find_label ?? k');
   @(lfl_IH s1 … IH1) [ /2/ ]
   cases (find_label ???)
@@ -641 +676 @@
 >FIND whd in ⊢ (% → ?); //
 qed.
 
+lemma swl_cost_state :
+ ∀g,f,us,s,k,k',e,m,cs.
+ cont_with_labels k k' →
+ state_with_labels_partial (State f (Scost cs s) k e m) (State (\fst (label_function g f)) (Scost cs (\fst (label_statement s us))) k' e m).
+#g #f #us #s #k #k' #e #m #cs #K
+cut (Scost cs (\fst (label_statement s us)) = \fst (label_statement (Scost cs s) us))
+[ normalize >shift_fst % ]
+#E >E @swl_state //
+qed.
+
+lemma ffs: ∀c.
+  None costlabel = None costlabel ∨ None costlabel = Some costlabel c.
+/2/
+qed.
+
 
 (* We show the main simulation in two stages.  First, we show it for all states
    in the relation *except* those for labeled_statements, then we'll show the
@@ -674 +724 @@
       ]
     | #u #s0 #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{0} whd
       whd in EX:(??%%); destruct /4/
-    | #ue #e0 #us0 #s0 #cl #cs #cpost #k0 #k0' #K #CL #_ #E1 #E2 #E3 destruct %{0}
+    | #ue #e0 #us0 #lb #s0 #lp #cs #cpost #k0 #k0' #K #LB #LP #_ #E1 #E2 #E3 destruct %{0}
       whd in EX:(??%%); destruct whd /4/
-    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
+    | #ue #e0 #us0 #lb #s0 #lp #cs #cpost #k0 #k0' #K #LB #LP #_ #E1 #E2 #E3 destruct
       cases (bindIO_inversion ??????? EX) -EX * #ve #tre * #EXe #EX
       cases (bindIO_inversion ??????? EX) -EX * * #EXb #EX
       normalize in EX; destruct
@@ -685 +735 @@
         whd in ⊢ (??%?); >EXe'
         whd in ⊢ (??%?); >label_expr_type >EXb
         whd % /4/
-      | %{2} whd
+      | cases LP #E destruct [ %{1} | %{0} ] whd
         whd in ⊢ (??%?); >EXe'
         whd in ⊢ (??%?); >label_expr_type >EXb
-        whd % [ <(E0_right tr) @twel_app /2/ | /4/ ]
+        whd % [  <(E0_right tr) @twel_app /2/ | *: /4/ ]
       ]
-    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
+    | #ue #e0 #us1 #st1 #us2 #lb #st2 #lp #cs #cpost #k0 #k0' #K #LB #LP #_ #E1 #E2 #E3 destruct
       whd in EX:(??%?); destruct
       %{0} whd /4/
-    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
+    | #ue #e0 #us1 #st1 #us2 #lb #st2 #lp #cs #cpost #k0 #k0' #K #LB #LP #_ #E1 #E2 #E3 destruct
       whd in EX:(??%?); destruct
       %{0} % /4/
-    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
+    | #ue #e0 #us1 #st1 #us2 #lb #st2 #lp #cs #cpost #k0 #k0' #K #LB #LP #_ #E1 #E2 #E3 destruct
       whd in EX:(??%?); destruct
       %{0} % /4/
     | #k0 #k0' #K #_ #E1 #E2 #E3 destruct
@@ -764 +814 @@
     whd in ⊢ (??%?); >EX1'
     whd in ⊢ (??%?); >label_expr_type >EX2
     whd in ⊢ (??%?); % [1,3: <(E0_right tr) ] /4/
-  | #a #st #cl #EX
+  | #a #lb #st #lp #EX
     cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
     cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
     normalize in EX; destruct
-    @blindly_label #u1 #u2 #cs #cpost * #CL destruct
+    @blindly_label #u1 #u2 #cs #cpost * #LB * #LP destruct
     cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 u1) #tr1' * #EX1' #T1
-    [ 1,2,3: %{1} | %{0} ] whd
+    [ 1,2,5,7: %{1} | *: %{0} ] whd
     whd in ⊢ (??%?); >EX1'
     whd in ⊢ (??%?); >label_expr_type >EX2
-    whd in ⊢ (??%?); whd % [ 1,3,5,7: <(E0_right tr) ] /5 by twel_new, swl_partial, swl_state, cwl_while, twel_app, or_introl, or_intror/
-  | #a #st #EX
+    whd in ⊢ (??%?); whd % [ 1,3,5,7: <(E0_right tr) @twel_app /2/ ]
+     (* faster than /4 by _/ but still not pleasant *)
+     try assumption try @twel_new % 
+     try ( @swl_cost_state @cwl_while // )
+     try ( @swl_state @cwl_while // )
+     @swl_state /2/
+  | #a #lb #st #lp #EX
     normalize in EX; destruct
-    whd in match (label_statement ??); @label_gen_elim #u1
-    @label_gen_elim #u2
-    whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6 >shift_fst
-    whd in match (add_cost_after ??); cases (fresh ??) #c7 #u7 >shift_fst
-    %{2} % /4/
-  | #st1 #a #st2 #st #EX
+    @blindly_label #u1 #u2 #cs #cpost * #LB #LP destruct
+    [ %{1} | %{0} ] whd % /5/
+  | #st1 #a #st2 #lb #st #lp #EX
     lapply (refl ? (is_Sskip st1)) cases (is_Sskip st1) in ⊢ (???% → ?); #Esk #Eskip
     whd in EX:(??%?); >Eskip in EX; #EX
-    whd in match (label_statement ??); @label_gen_elim #u1
-    @label_gen_elim #u2 @label_gen_elim #u3 @label_gen_elim #u4
-    whd in match (add_cost_before ??); cases (fresh ??) #c5 #u5 >shift_fst
-    whd in match (add_cost_after ??); cases (fresh ??) #c6 #u6 >shift_fst
+    @blindly_label #u1 #u2 #u3 #u4 #c3 #c4 #LB #LP
     [ cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
       cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
       normalize in EX; destruct
-      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
-      [ %{2} | %{3} ] whd
+      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 u2) #tr1' * #EX1' #T1
+      cases LB #LB cases LP #LP destruct
+      [ 1,2,5,7: %{1} | 3,4,6,8: %{0} ] whd
       whd in ⊢ (??%?); >EX1'
       whd in ⊢ (??%?); >label_expr_type >EX2
-      whd in ⊢ (??%?); % [ 1,3: <(E0_right tr) ] /4/
+      whd in ⊢ (??%?); % [ 1,3,5,7: <(E0_right tr) ]
+      /5 by twel_new, swl_partial, swl_state, cwl_for2, twel_app, or_introl, or_intror, swl_cost_state/
     | whd in EX:(??%%); destruct
-      %{1} whd
+      %{0} whd
       whd in ⊢ (??%?); cases (labelled_is_not_skip ? u1 Esk) #Esk' #Eskip'
-      >Eskip' whd in ⊢ (??%?); % /4/
+      >Eskip' whd in ⊢ (??%?); whd % /4/
     ]
   | #EX inversion KL
     [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     |#u #s0 #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
-    | #ue #e0 #us0 #s0 #cl #cs #cpost #k0 #k0' #K' * #CL #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
-    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
-    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
-    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
-    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
+    | #ue #e0 #us0 #lb #s0 #lp #cs #cpost #k0 #k0' #K' * #LB * #LP #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
+    | #ue #e0 #us0 #lb #s0 #lp #cs #cpost #k0 #k0' #K' * #LB * #LP #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
+    | #ue #e0 #us1 #s1 #us2 #lb #st2 #lp #cs #cpost #k0 #k0' #K' * #LB * #LP #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
+    | #ue #e0 #us1 #s1 #us2 #lb #st2 #lp #cs #cpost #k0 #k0' #K' * #LB * #LP #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
+    | #ue #e0 #us1 #s1 #us2 #lb #st2 #lp #cs #cpost #k0 #k0' #K' * #LB * #LP #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     | #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     | #ux #r #f0 #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     ]
     whd in match (label_statement ??);
-    [ 1,3,7,8: %{0} % /3/
-    | 2,5: %{1} whd % /3/
-    | 4,6: %{2} whd % /3/
+    [ 1,3,5,7,9,10,11,12,13,15,17,18,19: %{0} % /3/
+    | 2,4,6,8,14,16: %{1} whd % /3/
     ]
   | #EX inversion KL
     [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     |#u #s0 #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
-    | #ue #e0 #us0 #s0 #cl #cs #cpost #k0 #k0' #K' * #CL #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
-    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
-    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
-    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
-    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
+    | #ue #e0 #us0 #lb #s0 #lp #cs #cpost #k0 #k0' #K' * #LB * #LP #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
+    | #ue #e0 #us0 #lb #s0 #lp #cs #cpost #k0 #k0' #K' * #LB * #LP #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
+    | #ue #e0 #us1 #s1 #us2 #lb #st2 #lp #cs #cpost #k0 #k0' #K' * #LB * #LP #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
+    | #ue #e0 #us1 #s1 #us2 #lb #st2 #lp #cs #cpost #k0 #k0' #K' * #LB * #LP #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
+    | #ue #e0 #us1 #s1 #us2 #lb #st2 #lp #cs #cpost #k0 #k0' #K' * #LB * #LP #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     | #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     | #g #r #f0 #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     ]
     whd in match (label_statement ??);
-    [ 1,2,3,6,7,8: %{0} % /4/
-    | 5: %{1} % /4/
-    | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
+    [ 6,7,8,9:
+      cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
       cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
       normalize in EX; destruct
       cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ue) #tr1' * #EX1' #T1
-      [ %{0} | %{2} ] whd
+      [ 1,3,4,5,7,8: %{0} | *: %{1} ] whd
       whd in ⊢ (??%?); >EX1'
       whd in ⊢ (??%?); >label_expr_type >EX2
-      whd in ⊢ (??%?); % [ 3: <(E0_right tr) ] /3/
+      whd in ⊢ (??%?); % [ 13,15: <(E0_right tr) ] /4/
+    | *: %{0} whd % /5 by swl_partial, swl_state, swl_whilestate, cwl_for3, or_introl, or_intror/ 
     ]
   | * [2: #a ] #EX
     whd in EX:(??%?); cases (type_eq_dec (fn_return f) Tvoid) in EX;
@@ -867 +917 @@
     cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
     cases v1 in EX1 EX;
     [ 2: #sz #i #EX1 #EX
-    | *: normalize #A #B try #C destruct
+    | *: [ 2,4: #x ] #EX1 #EX whd in EX:(??%%); destruct
     ]
     whd in EX:(??%%); destruct 
     cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
@@ -896 +946 @@
   | #c #st #EX whd in EX:(??%?); destruct @blindly_label #u1
     %{0} % /3/
   ]
-| #u0 #f #ua #a #us #s #cl #cs #cpost #k #k' #e #m #K * #CL #EX
+| #u0 #f #ua #a #us #lb #s #lp #cs #cpost #k #k' #e #m #K * #LB * #LP #EX
   cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
   cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
   whd in EX:(??%%); destruct
   cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua) #tr1' * #EX1' #T1
-  [ 4: %{0} | 1,2,3: %{1} ] whd
+  [ 4,5,7,8: %{0} | *: %{1} ] whd
   whd in ⊢ (??%?); >EX1'
   whd in ⊢ (??%?); >label_expr_type >EX2
-  whd % [ 1,3,5,7: <(E0_right tr) ] /5/
-| #u0 #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX
+  whd % [ 9,11,13,15: <(E0_right tr) ] /5/
+| #u0 #f #ua #a #us #lb #s #lp #cs #cpost #k #k' #e #m #K * #LB * #LP #EX
   whd in EX:(??%%); destruct
-  %{1} % /4/
-| #u0 #f #ua2 #a2 #us3 #s3 #us #s #cs #cpost #k #k' #e #m #K #EX
+  [ 1,2: %{1} | *: %{0} ] % /5/
+| #u0 #f #ua2 #a2 #us3 #s3 #us #lb #s #lp #cs #cpost #k #k' #e #m #K * #LB * #LP #EX
   cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
   cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
   whd in EX:(??%%); destruct
   cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua2) #tr1' * #EX1' #T1
-  [ %{1} | %{2} ] whd
+  [ 1,2,3,6: %{1} | *: %{0} ] whd
   whd in ⊢ (??%?); >EX1'
   whd in ⊢ (??%?); >label_expr_type >EX2
-  % [1,3: <(E0_right tr) ] /4/
+  % [ 1,3,5,7: <(E0_right tr) ] try @swl_partial /5/
 | #u0 *
   [ #f #args #k #k' #m #K whd in ⊢ (??%? → ?); @pair_elim #e #m1 #EX1 #EX
     cases (bindIO_inversion ??????? EX) -EX #m2 * #EX2 #EX
@@ -948 +998 @@
       whd in EX:(??%%); destruct
       %{0} whd whd in ⊢ (??%?); >EX1 % /3/
     ]
-  | *: #A #B #C #D #E #F #G try #H try #I try #J try #L try #M try #N try #O
+  | *: #A #B #C #D #E #F #G try #H try #I try #J try #L try #M try #N try #O try #P try #Q try #R
        destruct whd in EX:(??%?); destruct
   ]
 | #r #EX whd in EX:(??%%); destruct
@@ -990 +1040 @@
   ∃f,argtys,retty,vargs,k',m. s = Callstate (CL_External f argtys retty) vargs k' m.
 #ge #s cases s
 [ #f #st #kk #e #m #o #k #EX @⊥ cases st in EX ⊢ %;
-  [ 11,14: #a | 2,4,7,12,13,15: #a #b | 3,5,6: #a #b #c | 8: #a #b #c #d ]
+  [ 11,14: #a | 2,4,12,13,15: #a #b | 3,5: #a #b #c | 6,7: #a #b #c #d | 8: #a #b #c #d #e #f ]
   whd in ⊢ (??%? → ?);
-  [ 4,5,7,8: #EX destruct ]
+  [ 4,6,7,11: #EX destruct ]
   [ cases a 
     [ whd in ⊢ (??%? → ?); cases (fn_return f) normalize #A try #B try #C try #D destruct
     | #a' whd nodelta in ⊢ (??%? → ?); cases (type_eq_dec (fn_return f) Tvoid)
@@ -1006 +1056 @@
   | 6,7: @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 #EX whd in EX:(??%?); destruct
   | cases (is_Sskip a) #H [ @bindIO_res_interact #vt #Evt @bindIO_res_interact #v #Ev ] #EX whd in EX:(??%?); destruct
   | cases kk [ 1,8: cases (fn_return f) normalize #A try #B try #C try #D try #E try #F try #G try #H destruct
-    | 2,3,5,6,7: normalize #A #B try #C try #D try #E destruct
-    | #z1 #z2 #z3 @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 cases x3 #EX whd in EX:(??%?); destruct ]
-  | cases kk normalize #A try #B try #C try #D try #E destruct
-  | cases kk [ 4: #z1 #z2 #z3 @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 cases x3 #EX whd in EX:(??%?); destruct
-    | *: normalize #A try #B try #C try #D try #E destruct
+    | 2,3,5,6,7: normalize #A #B try #C try #D try #E try #F try #G destruct
+    | #z1 #z2 #z3 #z4 #z5 @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 cases x3 #EX whd in EX:(??%?); destruct ]
+  | cases kk normalize #A try #B try #C try #D try #E try #F try #G destruct
+  | cases kk [ 4: #z1 #z2 #z3 #z4 #z5 @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 cases x3 #EX whd in EX:(??%?); destruct
+    | *: normalize #A try #B try #C try #D try #E try #F try #G destruct
     ]
   ]
 | #f #args #kk #m #o #k cases f 
@@ -1027 +1077 @@
     | 8: #x1 #x2 #x3 #x4 cases x1
       [ whd in ⊢ (??%? → ?); #EX destruct | #x5 whd in ⊢ (??%? → ?); cases x5
           #x6 #x7 @bindIO_opt_interact #m' #Em #EX whd in EX:(??%?); destruct ]
-    | *: normalize #A try #B try #C try #D try #E destruct ]
+    | *: normalize #A try #B try #C try #D try #E try #F try #G destruct ]
 | #r #o #k #EX whd in EX:(??%?); destruct
 ] qed.
 
@@ -1037 +1087 @@
 #f #a #k #m #s1 #S inversion S
 [ #s #s' #S' #E1 #E2 #E3 destruct inversion S'
   [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 destruct
-  | #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct
-  | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 destruct
-  | #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 destruct
+  | #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 destruct
+  | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 destruct
+  | #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H66 #H67 destruct
   | #u0 #f' #a' #k' #k'' #m' #K #E1 #E2 #E3 destruct %{k''} % /2/
   | #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct
   | #H72 #H73 #H74 #H75 destruct

src/Clight/switchRemoval.ma

@@ -76 +76 @@
 | Scall _ _ _ ⇒ True
 | Ssequence s1 s2 ⇒ switch_free s1 ∧ switch_free s2
 | Sifthenelse e s1 s2 ⇒ switch_free s1 ∧ switch_free s2
-| Swhile e body _ ⇒ switch_free body
-| Sdowhile e body ⇒ switch_free body
-| Sfor s1 _ s2 s3 ⇒ switch_free s1 ∧ switch_free s2 ∧ switch_free s3
+| Swhile e _ body _ ⇒ switch_free body
+| Sdowhile e _ body _ ⇒ switch_free body
+| Sfor s1 _ s2 _ s3 _ ⇒ switch_free s1 ∧ switch_free s2 ∧ switch_free s3
 | Sbreak ⇒ True
 | Scontinue ⇒ True
 | Sreturn _ ⇒ True
@@ -122 +122 @@
   Ssequence (convert_break_to_goto s1 lab) (convert_break_to_goto s2 lab)
 | Sifthenelse e iftrue iffalse ⇒
   Sifthenelse e (convert_break_to_goto iftrue lab) (convert_break_to_goto iffalse lab)
-| Sfor init e update body ⇒
-  Sfor (convert_break_to_goto init lab) e update body
+| Sfor init e update lb body lp ⇒
+  Sfor (convert_break_to_goto init lab) e update lb body lp
 | Slabel l body ⇒
   Slabel l (convert_break_to_goto body lab)
 | Scost cost body ⇒
@@ -136 +136 @@
 #s elim s //
 [ 1: #s1 #s2 #Hind1 #Hind2 #label * #Hsf1 #Hsf2 /3/
 | 2: #e #s1 #s2 #Hind1 #Hind2 #label * #Hsf1 #Hsf2 /3/
-| 3: #s1 #e #s2 #s3 #Hind1 #Hind2 #Hind3 #label * * #Hsf1 #Hsf2 #Hsf3 normalize
+| 3: #s1 #e #s2 #lb #s3 #lp #Hind1 #Hind2 #Hind3 #label * * #Hsf1 #Hsf2 #Hsf3 normalize
      try @conj try @conj /3/
 | 4: #l #s0 #Hind #lab #Hsf whd in Hsf; normalize /2/
 | 5: #l #s0 #Hind #lab #Hsf whd in Hsf; normalize /3/
@@ -247 +247 @@
   do 〈s1', acc1, fvs', u'〉 ← switch_removal s1 fvs u;
   do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u';
   ret 〈Sifthenelse e s1' s2', acc1 @ acc2, fvs'', u''〉
-| Swhile e body cl ⇒
+| Swhile e lb body lp ⇒
   do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
-  ret 〈Swhile e body' cl, acc, fvs', u'〉
-| Sdowhile e body ⇒
+  ret 〈Swhile e lb body' lp, acc, fvs', u'〉
+| Sdowhile e lb body lp ⇒
   do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
-  ret 〈Sdowhile e body', acc, fvs', u'〉
-| Sfor s1 e s2 s3 ⇒
+  ret 〈Sdowhile e lb body' lp, acc, fvs', u'〉
+| Sfor s1 e s2 lb s3 lp ⇒
   do 〈s1', acc1, fvs', u'〉 ← switch_removal s1 fvs u;
   do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u';
   do 〈s3', acc3, fvs''', u'''〉 ← switch_removal s3 fvs'' u'';
-  ret 〈Sfor s1' e s2' s3', acc1 @ acc2 @ acc3, fvs''', u'''〉
+  ret 〈Sfor s1' e s2' lb s3' lp, acc1 @ acc2 @ acc3, fvs''', u'''〉
 | Sbreak ⇒
   ret 〈st, [ ], fvs, u〉
 | Scontinue ⇒
@@ -316 +316 @@
   let 〈fvs, u'〉 ≝ mk_fresh_variables s1 u in
   let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in
   〈fvs @ fvs', u''〉
-| Swhile e body cl ⇒
+| Swhile e _ body _ ⇒
   mk_fresh_variables body u
-| Sdowhile e body ⇒
+| Sdowhile e _ body _ ⇒
   mk_fresh_variables body u
-| Sfor s1 e s2 s3 ⇒
+| Sfor s1 e s2 _ s3 _ ⇒
   let 〈fvs, u'〉 ≝ mk_fresh_variables s1 u in
   let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in
   let 〈fvs'', u'''〉 ≝ mk_fresh_variables s3 u'' in
@@ -365 +365 @@
   (Sca:∀eo,e,args. P (Scall eo e args))
   (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
   (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
-  (Swh:∀e,s,cl. P s → P (Swhile e s cl))
-  (Sdo:∀e,s. P s → P (Sdowhile e s))
-  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
+  (Swh:∀e,s,lb,lp. P s → P (Swhile e lb s lp))
+  (Sdo:∀e,s,lb,lp. P s → P (Sdowhile e lb s lp))
+  (Sfo:∀s1,e,s2,s3,lb,lp. P s1 → P s2 → P s3 → P (Sfor s1 e s2 lb s3 lp))
   (Sbr:P Sbreak)
   (Sco:P Scontinue)
   (Sre:∀eo. P (Sreturn eo))
@@ -388 +388 @@
 | Sifthenelse e s1 s2 ⇒ Sif e s1 s2
     (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
     (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
-| Swhile e s cl ⇒ Swh e s cl
+| Swhile e lb s lp ⇒ Swh e s lb lp
     (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
-| Sdowhile e s ⇒ Sdo e s
+| Sdowhile e lb s lp ⇒ Sdo e s lb lp
     (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
-| Sfor s1 e s2 s3 ⇒ Sfo s1 e s2 s3
+| Sfor s1 e s2 lb s3 lp ⇒ Sfo s1 e s2 s3 lb lp
     (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
     (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
     (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s3)
@@ -414 +414 @@
   (Sca:∀eo,e,args. P (Scall eo e args))
   (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
   (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
-  (Swh:∀e,s,cl. P s → P (Swhile e s cl))
-  (Sdo:∀e,s. P s → P (Sdowhile e s))
-  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
+  (Swh:∀e,s,lb,lp. P s → P (Swhile e lb s lp))
+  (Sdo:∀e,s,lb,lp. P s → P (Sdowhile e lb s lp))
+  (Sfo:∀s1,e,s2,s3,lb,lp. P s1 → P s2 → P s3 → P (Sfor s1 e s2 lb s3 lp))
   (Sbr:P Sbreak)
   (Sco:P Scontinue)
   (Sre:∀eo. P (Sreturn eo))
@@ -470 +470 @@
          (Sifthenelse e (ret_st statement s1') (ret_st statement s2'))
          (ret_acc statement s1'@ret_acc statement s2') (ret_fvs statement s2')
          (ret_u statement s2')))} % try //
-| 6: #e #s #cl #H #u0 #u1 #post normalize
+| 6: #e #s #lb #lp #H #u0 #u1 #post normalize
      elim (H u0 u1 post) #s1' * normalize
      cases (mk_fresh_variables s u0) #fvs #u'
      #Heq1 #Heq1_fvs >Heq1 normalize nodelta
-     %{(mk_swret statement (Swhile e (ret_st statement s1') cl) (ret_acc statement s1')
+     %{(mk_swret statement (Swhile e lb (ret_st statement s1') lp) (ret_acc statement s1')
         (ret_fvs statement s1') (ret_u statement s1'))} % try //
-| 7: #e #s #H #u0 #u1 #post normalize
+| 7: #e #s #lb #lp #H #u0 #u1 #post normalize
      elim (H u0 u1 post) #s1' * normalize
      cases (mk_fresh_variables s u0) #fvs #u'
      #Heq1 #Heq1_fvs >Heq1 normalize nodelta
-     %{(mk_swret statement (Sdowhile e (ret_st statement s1')) (ret_acc statement s1')
+     %{(mk_swret statement (Sdowhile e lb (ret_st statement s1') lp) (ret_acc statement s1')
         (ret_fvs statement s1') (ret_u statement s1'))} % try //
-| 8: #s1 #e #s2 #s3 #H1 #H2 #H3 #u0 #u1 #post normalize
+| 8: #s1 #e #s2 #s3 #lb #lp #H1 #H2 #H3 #u0 #u1 #post normalize
      elim (H1 u0 u1
                 (\fst (mk_fresh_variables s2 (\snd  (mk_fresh_variables s1 u0))) @
                 (\fst (mk_fresh_variables s3 (\snd  (mk_fresh_variables s2 (\snd (mk_fresh_variables s1 u0)))))) @
@@ -497 +497 @@
      >associative_append >associative_append >Heq1 normalize >Heq1_fvs
      >Heq2 normalize >Heq2_fvs >Heq3 normalize
      %{(mk_swret statement
-        (Sfor (ret_st statement s1') e (ret_st statement s2') (ret_st statement s3'))
+        (Sfor (ret_st statement s1') e (ret_st statement s2') lb (ret_st statement s3') lp)
         (ret_acc statement s1'@ret_acc statement s2'@ret_acc statement s3')
         (ret_fvs statement s3') (ret_u statement s3'))} % try //
 | 9:  #u0 #u1 #post normalize %{(mk_swret statement Sbreak [] post u1)} % //
@@ -626 +626 @@
   max_id (max_of_statement s1) (max_of_statement s2)
 | Sifthenelse e s1 s2 ⇒
   max_id (max_of_expr e) (max_id (max_of_statement s1) (max_of_statement s2))
-| Swhile e body _ ⇒
+| Swhile e _ body _ ⇒
   max_id (max_of_expr e) (max_of_statement body)
-| Sdowhile e body ⇒
+| Sdowhile e _ body _ ⇒
   max_id (max_of_expr e) (max_of_statement body)
-| Sfor init test incr body ⇒
+| Sfor init test incr _ body _ ⇒
   max_id (max_id (max_of_statement init) (max_of_expr test)) (max_id (max_of_statement incr) (max_of_statement body))
 | Sbreak ⇒ least_identifier
 | Scontinue ⇒ least_identifier
@@ -710 +710 @@
   ]
 | Ssequence sub1 sub2 ⇒ P sub1 ∧ P sub2
 | Sifthenelse e sub1 sub2 ⇒ P sub1 ∧ P sub2
-| Swhile e sub _ ⇒ Q e ∧ P sub
-| Sdowhile e sub ⇒ Q e ∧ P sub
-| Sfor sub1 cond sub2 sub3 ⇒ P sub1 ∧ Q cond ∧ P sub2 ∧ P sub3
+| Swhile e _ sub _ ⇒ Q e ∧ P sub
+| Sdowhile e _ sub _ ⇒ Q e ∧ P sub
+| Sfor sub1 cond sub2 _ sub3 _ ⇒ P sub1 ∧ Q cond ∧ P sub2 ∧ P sub3
 | Sbreak ⇒ True
 | Scontinue ⇒ True
 | Sreturn r ⇒
@@ -1414 +1414 @@
     switch_cont_sim fvs k k' →
     switch_removal s fvs u = Some ? result →
     switch_cont_sim fvs (Kseq s k) (Kseq (ret_st ? result) k')
-| swc_while : ∀fvs,e,s,cl,k,k',u,result.
-    fresh_for_statement (Swhile e s cl) u →
+| swc_while : ∀fvs,e,lb,s,lp,k,k',u,result.
+    fresh_for_statement (Swhile e lb s lp) u →
     switch_cont_sim fvs k k' →
     switch_removal s fvs u = Some ? result →
-    switch_cont_sim fvs (Kwhile e s cl k) (Kwhile e (ret_st ? result) cl k')
-| swc_dowhile : ∀fvs,e,s,k,k',u,result.
-    fresh_for_statement (Sdowhile e s) u →
+    switch_cont_sim fvs (Kwhile e lb s lp k) (Kwhile e lb (ret_st ? result) lp k')
+| swc_dowhile : ∀fvs,e,lb,s,lp,k,k',u,result.
+    fresh_for_statement (Sdowhile e lb s lp) u →
     switch_cont_sim fvs k k' →
     switch_removal s fvs u = Some ? result →
-    switch_cont_sim fvs (Kdowhile e s k) (Kdowhile e (ret_st ? result) k')
-| swc_for1 : ∀fvs,e,s1,s2,k,k',u,result.
-    fresh_for_statement (Sfor Sskip e s1 s2) u →
+    switch_cont_sim fvs (Kdowhile e lb s lp k) (Kdowhile e lb (ret_st ? result) lp k')
+| swc_for1 : ∀fvs,e,s1,lb,s2,lp,k,k',u,result.
+    fresh_for_statement (Sfor Sskip e s1 lb s2 lp) u →
     switch_cont_sim fvs k k' →
-    switch_removal (Sfor Sskip e s1 s2) fvs u = Some ? result →
-    switch_cont_sim fvs (Kseq (Sfor Sskip e s1 s2) k) (Kseq (ret_st ? result) k')
-| swc_for2 : ∀fvs,e,s1,s2,k,k',u,result1,result2.
-    fresh_for_statement (Sfor Sskip e s1 s2) u →
+    switch_removal (Sfor Sskip e s1 lb s2 lp) fvs u = Some ? result →
+    switch_cont_sim fvs (Kseq (Sfor Sskip e s1 lb s2 lp) k) (Kseq (ret_st ? result) k')
+| swc_for2 : ∀fvs,e,s1,lb,s2,lp,k,k',u,result1,result2.
+    fresh_for_statement (Sfor Sskip e s1 lb s2 lp) u →
     switch_cont_sim fvs k k' →
     switch_removal s1 fvs u = Some ? result1 →
     switch_removal s2 fvs (ret_u ? result1) = Some ? result2 →
-    switch_cont_sim fvs (Kfor2 e s1 s2 k) (Kfor2 e (ret_st ? result1) (ret_st ? result2) k')
-| swc_for3 : ∀fvs,e,s1,s2,k,k',u,result1,result2.
-    fresh_for_statement (Sfor Sskip e s1 s2) u →
+    switch_cont_sim fvs (Kfor2 e s1 lb s2 lp k) (Kfor2 e (ret_st ? result1) lb (ret_st ? result2) lp k')
+| swc_for3 : ∀fvs,e,s1,lb,s2,lp,k,k',u,result1,result2.
+    fresh_for_statement (Sfor Sskip e s1 lb s2 lp) u →
     switch_cont_sim fvs k k' →
     switch_removal s1 fvs u = Some ? result1 →
     switch_removal s2 fvs (ret_u ? result1) = Some ? result2 ->
-    switch_cont_sim fvs (Kfor3 e s1 s2 k) (Kfor3 e (ret_st ? result1) (ret_st ? result2) k')
+    switch_cont_sim fvs (Kfor3 e s1 lb s2 lp k) (Kfor3 e (ret_st ? result1) lb (ret_st ? result2) lp k')
 | swc_switch : ∀fvs,k,k'.
     switch_cont_sim fvs k k' → 
     switch_cont_sim fvs (Kswitch k) (Kswitch k')

src/Clight/test/factorial.c.ma

@@ -24 +24 @@
               (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
               (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
               (Tint I32 Signed  )))
+          (None ?)
           (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
             (Expr (Ebinop Omul
               (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
               (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  )))
               (Tint I32 Signed  )))
-        )
+        (None ?))
         (Sreturn (Some expr (Expr (Evar (ident_of_nat 3))
                               (Tint I32 Signed  )))))))
       

src/Clight/test/insertsort.c.ma

@@ -121 +121 @@
       (Ssequence
       (Swhile (Expr (Evar (ident_of_nat 2))
                 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
+        (None ?)
         (Ssequence
         (Sassign (Expr (Evar (ident_of_nat 15))
                    (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
@@ -141 +142 @@
           (Expr (Eaddrof
             (Expr (Evar (ident_of_nat 16))
               (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
-            (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))]))))
+            (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))])))
+        (None ?))
       (Sassign (Expr (Ederef
                  (Expr (Evar (ident_of_nat 17))
                    (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))))
@@ -172 +174 @@
       (Ssequence
       (Swhile (Expr (Evar (ident_of_nat 20))
                 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
+        (None ?)
         (Ssequence
         (Scall (None expr) (Expr (Evar (ident_of_nat 18))
                              (Tfunction (Tcons (Tint I8 Unsigned ) Tnil) Tvoid)) 
@@ -186 +189 @@
                           (Expr (Evar (ident_of_nat 20))
                             (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
                           (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))) (ident_of_nat 2))
-            (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))))
+            (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))))
+        (None ?))
       (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0))
                             (Tint I32 Signed  )))))))
     

src/Clight/test/runtime.c.ma

@@ -20 +20 @@
                    (Expr (Ecast (Tint I32 Unsigned)
                      (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
                      (Tint I32 Unsigned))) (Tint I32 Unsigned))
+           (None ?)
            (Ssequence
            (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Unsigned))
              (Expr (Ebinop Osub
@@ -34 +35 @@
                    (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
                    (Tint I32 Signed  ))
                  (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
-                 (Tint I32 Signed  ))) (Tint I8 Unsigned )))))
+                 (Tint I32 Signed  ))) (Tint I8 Unsigned ))))
+           (None ?))
          (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
                                (Expr (Evar (ident_of_nat 2))
                                  (Tint I8 Unsigned ))) (Tint I32 Signed  )))))))

src/Clight/test/search.c.ma

@@ -26 +26 @@
                    (Expr (Ecast (Tint I32 Signed  )
                      (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
                      (Tint I32 Signed  ))) (Tint I32 Signed  ))
+           (None ?)
            (Ssequence
            (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))
              (Expr (Ecast (Tint I8 Unsigned )
@@ -103 +104 @@
                      (Tint I32 Signed  ))
                    (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
                    (Tint I32 Signed  ))) (Tint I8 Unsigned )))
-             Sskip)))))
+             Sskip))))
+           (None ?))
          (Sreturn (Some expr (Expr (Ecast (Tint I8 Unsigned )
                                (Expr (Eunop Oneg (Expr (Econst_int I32 (repr ? 1))
                                                    (Tint I32 Signed  )))

src/Clight/test/sum.c.ma

@@ -27 +27 @@
              (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
              (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
              (Tint I32 Signed  )))
+         (None ?)
          (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))
            (Expr (Ecast (Tint I8 Unsigned )
              (Expr (Ebinop Oadd
@@ -42 +43 @@
                      (Tpointer (Tint I8 Unsigned )))) (Tint I8 Unsigned )))
                  (Tint I32 Signed  ))) (Tint I32 Signed  )))
              (Tint I8 Unsigned )))
-       )
+       (None ?))
        (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
                              (Expr (Evar (ident_of_nat 3))
                                (Tint I8 Unsigned ))) (Tint I32 Signed  ))))))

src/Clight/toCminor.ma

@@ -50 +50 @@
 | Sifthenelse e1 s1 s2 ⇒ gather_mem_vars_expr e1 ∪
                          gather_mem_vars_stmt s1 ∪
                          gather_mem_vars_stmt s2
-| Swhile e1 s1 _ ⇒ gather_mem_vars_expr e1 ∪
-                   gather_mem_vars_stmt s1
-| Sdowhile e1 s1 ⇒ gather_mem_vars_expr e1 ∪
-                   gather_mem_vars_stmt s1
-| Sfor s1 e1 s2 s3 ⇒ gather_mem_vars_stmt s1 ∪
-                     gather_mem_vars_expr e1 ∪
-                     gather_mem_vars_stmt s2 ∪
-                     gather_mem_vars_stmt s3
+| Swhile e1 _ s1 _ ⇒ gather_mem_vars_expr e1 ∪
+                     gather_mem_vars_stmt s1
+| Sdowhile e1 _ s1 _ ⇒ gather_mem_vars_expr e1 ∪
+                       gather_mem_vars_stmt s1
+| Sfor s1 e1 s2 _ s3 _ ⇒ gather_mem_vars_stmt s1 ∪
+                        gather_mem_vars_expr e1 ∪
+                        gather_mem_vars_stmt s2 ∪
+                        gather_mem_vars_stmt s3
 | Sbreak ⇒ ∅
 | Scontinue ⇒ ∅
 | Sreturn oe1 ⇒ match oe1 with [ None ⇒ ∅ | Some e1 ⇒ gather_mem_vars_expr e1 ]
@@ -925 +925 @@
 match s with
 [ Ssequence s1 s2 ⇒ labels_defined s1 @ labels_defined s2
 | Sifthenelse _ s1 s2 ⇒ labels_defined s1 @ labels_defined s2
-| Swhile _ s _ ⇒ labels_defined s
-| Sdowhile _ s ⇒ labels_defined s
-| Sfor s1 _ s2 s3 ⇒ labels_defined s1 @ labels_defined s2 @ labels_defined s3
+| Swhile _ _ s _ ⇒ labels_defined s
+| Sdowhile _ _ s _ ⇒ labels_defined s
+| Sfor s1 _ s2 _ s3 _ ⇒ labels_defined s1 @ labels_defined s2 @ labels_defined s3
 | Sswitch _ ls ⇒ labels_defined_switch ls
 | Slabel l s ⇒ l::(labels_defined s)
 | Scost _ s ⇒ labels_defined s
@@ -1126 +1126 @@
 definition optional_cost : option costlabel → stmt → stmt ≝
 λo,s. match o with [ Some l ⇒ St_cost l s | None ⇒ s ].
 
+lemma optional_cost_P : ∀s,cl,P.
+  (∀c. P (St_cost c s)) →
+  stmt_P P s →
+  stmt_P P (optional_cost cl s).
+#s * /2/
+qed.
+
 let rec translate_statement (vars:var_types) (uv:tmpgen vars) (ul:labgen) (lbls:lenv) (flag:convert_flag) (rettyp:option typ) (s:statement) on s 
   : res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag rettyp su) ≝
 match s return λs.res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag rettyp su) with
@@ -1168 +1175 @@
         OK ? «〈fgens2, St_ifthenelse ?? e1' s1' s2'〉, ?»
     | _ ⇒ λ_.Error ? (msg TypeMismatch)
     ] e1'
-| Swhile e1 s1 cl ⇒
+| Swhile e1 lb s1 lp ⇒
     do e1' ← translate_expr vars e1;
     match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
     [ ASTint _ _ ⇒ λe1'.         
@@ -1178 +1185 @@
         do «fgens2, s1',H1» ← translate_statement vars uv ul1 lbls (ConvertTo entry exit) rettyp s1;
         let converted_loop ≝
           St_label entry
-            (St_ifthenelse ?? e1' (St_seq s1' (St_goto entry)) (St_label exit (optional_cost cl St_skip)))
+            (St_ifthenelse ?? e1' (St_seq (optional_cost lb s1') (St_goto entry)) (St_label exit (optional_cost lp St_skip)))
         in         
           OK ? «〈fgens2, converted_loop〉, ?»
     | _ ⇒ λ_.Error ? (msg TypeMismatch)
     ] e1'
-| Sdowhile e1 s1 ⇒
+| Sdowhile e1 lb s1 lp ⇒
     do e1' ← translate_expr vars e1;
     match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with
     [ ASTint _ _ ⇒ λe1'.
@@ -1192 +1199 @@
         do «fgens2, s1', H1» ← translate_statement vars uv ul1 lbls (ConvertTo entry exit) rettyp s1;
         let converted_loop ≝
           St_label entry
-           (St_seq
+           (optional_cost lb
              (St_seq 
                s1' 
-               (St_ifthenelse ?? e1' (St_goto entry) St_skip)
+               (St_ifthenelse ?? e1' (St_goto entry) (St_label exit (optional_cost lp St_skip)))
              )
-             (St_label exit St_skip))
+           )
         in
         (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
         OK ? «〈fgens2, converted_loop〉, ?»
     | _ ⇒ λ_.Error ? (msg TypeMismatch)
     ] e1'
-| Sfor s1 e1 s2 s3 ⇒
+| Sfor s1 e1 s2 lb s3 lp ⇒
     do e1' ← translate_expr vars e1;
     match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with
     [ ASTint _ _ ⇒ λe1'.
@@ -1217 +1224 @@
           St_seq
             s1'
             (St_label entry
-              (St_seq
-                (St_ifthenelse ?? e1' (St_seq s3' (St_seq s2' (St_goto entry))) St_skip)
-                (St_label exit St_skip)
-            ))
+              (St_ifthenelse ?? e1' (optional_cost lb (St_seq s3' (St_seq s2' (St_goto entry)))) (St_label exit (optional_cost lp St_skip)))
+            )
         in 
           OK ? «〈fgens4, converted_loop〉, ?»
     | _ ⇒ λ_.Error ? (msg TypeMismatch)
@@ -1338 +1343 @@
      #l * try * [ 1,4: #H %1 %1 normalize in H ⊢ %; try (@Exists_append_l @H); try (@Exists_append_r @H)
                 | 2,5: #H %1 %2 assumption
                 | 3,6: #H %2 assumption ] ]
-try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I try assumption
-[ 1,10,20: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
-| cases cl normalize /3/
+try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj
+try ( @optional_cost_P try @(λ_.I) try @conj try @conj try @conj try @conj try @conj
+  try ( @optional_cost_P try @(λ_.I) try @conj try @conj try @conj try @conj try @conj ))
+try @I try assumption
+[ 1,7,17: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
 | (*2,8: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) //
-|*) 3,11: whd #l #H normalize in H;
+|*) 2,8: whd #l #H normalize in H;
          elim (Hlabels_tr1 … H) #label #Hlabel @(ex_intro … label)
          @conj
          [ 1,3: @(proj1 … Hlabel)
-         | 2,4: whd @or_intror normalize @Exists_append_l @Exists_append_l try @Exists_append_l
+         | 2,4: whd cases lb [ 2,4: #lb'] @or_intror @Exists_append_l try @Exists_append_l try @Exists_append_l
               @(proj2 … Hlabel) ]
-| 30: whd %2 %2 whd /2/
-| 31: whd %2 whd /2/
-| cases cl normalize /3/
-| 5,17: whd %1 %1 normalize /2/
-| 6,13: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
-   #l * try * [ 1,5: #H %1 %1 normalize %2 @Exists_append_l @Exists_append_l try @Exists_append_l @H
+| 3,5,9,11,14: whd %1 %1 normalize /2/
+| 4,12: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
+   #l * try * [ 1,5: #H %1 %1 normalize cases lb [2,4: #lb' ] %2 @Exists_append_l try @Exists_append_l try @Exists_append_l @H
               | 2,6: #H %1 %2 assumption
               | 3,7: #H <H %1 %1 normalize /2/
-              | 4,8: #H normalize in H; elim H [ 1,3: #E <E %1 %1 normalize %2
+              | 4,8: #H normalize in H; elim H [ 1,3: #E <E %1 %1 normalize cases lb [ 2,4: #lb' ] %2
                                                  @Exists_append_r normalize /2/
                                                | 2,4: * ]
               ]
-| 7: normalize %1 %1 %1 //
-| 8,15: normalize %1 %1 %2 @Exists_append_r normalize /2/
-| cases cl normalize /3/
-| 12,14: whd %1 %1 normalize /2/
-| 16: whd #label * [ 1: #Eq @(ex_intro … l') @conj [ 1: destruct // | whd /2/ ]
-                   | 2: #H elim (Hlabels_tr1 label H)
-                         #lab * #Hlookup #Hdef @(ex_intro … lab) @conj
-                         [ 1: // | 2: whd %2 assumption ]
-                   ]
-| 18: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
+| 6,10: normalize %1 %1 %2 cases lb [2,4:#lb'] @Exists_append_r normalize /2/
+| whd #label * [ 1: #Eq @(ex_intro … l') @conj [ 1: destruct // | whd /2/ ]
+               | 2: #H elim (Hlabels_tr1 label H)
+                     #lab * #Hlookup #Hdef @(ex_intro … lab) @conj
+                     [ 1: // | 2: whd %2 assumption ]
+               ]
+| @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
    #l * try * [ 1: #H %1 %1 normalize %2 @H
               | 2: #H %1 %2 assumption
               | 3: #H %2 assumption ]
-| 19: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
-   #H @(Htmps_pres3 … (Htmps_pres2 … H))
-| 21: @(stmt_P_mp … Hstmt_inv2) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
-   #H @(Htmps_pres3 … H)
-| 22: whd #l #H normalize in H;
-      cases (Exists_append … H) #Hcase
-      [ 1: elim (Hlabels_tr1 l Hcase) #label #Hlabel @(ex_intro … label) @conj
-        [ 1: @(proj1 … Hlabel)
-        | 2: normalize @Exists_append_l @(proj2 … Hlabel)
-        ]
-      | 2: cases (Exists_append … Hcase) #Hcase2
-        [ 1: elim (Hlabels_tr2 l Hcase2) #label #Hlabel @(ex_intro … label) @conj
-          [ 1: @(proj1 … Hlabel)
-          | 2: normalize >append_nil >append_nil >append_cons
-               @Exists_append_r @Exists_append_l @Exists_append_r
-               @(proj2 … Hlabel)
-          ]
-        | 2: elim (Hlabels_tr3 l Hcase2) #label #Hlabel @(ex_intro … label) @conj
-          [ 1: @(proj1 … Hlabel)
-          | 2: normalize >append_nil >append_nil >append_cons
-             @Exists_append_r @Exists_append_l @Exists_append_l
-             @(proj2 … Hlabel)
-          ]
-        ]
+| @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
+  #H @(Htmps_pres3 … (Htmps_pres2 … H))
+| @(stmt_P_mp … Hstmt_inv2) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
+  #H @(Htmps_pres3 … H)
+| whd #l #H normalize in H;
+  cases (Exists_append … H) #Hcase
+  [ elim (Hlabels_tr1 l Hcase) #label #Hlabel @(ex_intro … label) @conj
+    [ @(proj1 … Hlabel)
+    | normalize @Exists_append_l @(proj2 … Hlabel)
+    ]
+  | cases (Exists_append … Hcase) #Hcase2
+    [ elim (Hlabels_tr2 l Hcase2) #label #Hlabel %{label} %
+      [ @(proj1 … Hlabel)
+      | normalize cases lb [2:#lb'] normalize >append_nil >append_cons
+        @Exists_append_r @Exists_append_l @Exists_append_r
+        @(proj2 … Hlabel)
       ]
-| 23: #id #ty #H @(Htmps_pres3 … (Htmps_pres2 … (Htmps_pres1 … H)))
-| 24: @(stmt_P_mp … Hind3) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
+    | 2: elim (Hlabels_tr3 l Hcase2) #label #Hlabel @(ex_intro … label) @conj
+      [ 1: @(proj1 … Hlabel)
+      | 2: normalize cases lb [2:#lb'] normalize >append_nil >append_cons
+         @Exists_append_r @Exists_append_l @Exists_append_l
+         @(proj2 … Hlabel)
+      ]
+    ]
+  ]
+| #id #ty #H @(Htmps_pres3 … (Htmps_pres2 … (Htmps_pres1 … H)))
+| @(stmt_P_mp … Hind3) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
    #l * try * [ 1: #H %1 %1 normalize @Exists_append_l @H
               | 2: #H %1 %2 assumption
               | 3: #H %2 assumption ]
-| 25: whd %1 %1 normalize /2/
-| 26: @(stmt_P_mp … Hind1) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
-   #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?))
-                   @Exists_append_r @Exists_append_l @Exists_append_l 
+| 22,23: whd %1 %1 normalize /2/
+| @(stmt_P_mp … Hind2) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
+   #l * try * [ 1: #H %1 %1 normalize cases lb [2:#lb'] normalize @Exists_append_r @(Exists_add ?? (nil ?))
+                   @Exists_append_r @Exists_append_l @Exists_append_r
                    @Exists_append_l assumption
               | 2: #H %1 %2 assumption
               | 3: #H <H %1 %1 normalize
                    @Exists_append_r whd %1 //
-              | 4: * [ 1: #H <H %1 %1 normalize
-                       @Exists_append_r @(Exists_add ?? (nil ?))
-                       @Exists_append_r @Exists_append_r
-                       whd %1 //
+              | 4: * [ 1: #Eq <Eq %1 %1 whd normalize
+                       @Exists_append_r @(Exists_add ?? (nil ?)) @Exists_append_r
+                       @Exists_append_r whd %1 //
                      | 2: * ]
               ]
-| 27: @(stmt_P_mp … Hind2) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
-   #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?))
-                   @Exists_append_r @Exists_append_l @Exists_append_l                    
-                   @Exists_append_r @Exists_append_l assumption
+| @(stmt_P_mp … Hind1) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
+   #l * try * [ 1: #H %1 %1 normalize cases lb [2:#lb'] normalize @Exists_append_r @(Exists_add ?? (nil ?))
+                   @Exists_append_r @Exists_append_l
+                   @Exists_append_l assumption
               | 2: #H %1 %2 assumption
               | 3: #H <H %1 %1 normalize
                    @Exists_append_r whd %1 //
-              | 4: * [ 1: #Eq <Eq %1 %1 whd normalize
-                       @Exists_append_r @(Exists_add ?? (nil ?)) @Exists_append_r
-                       @Exists_append_r whd %1 //
+              | 4: * [ 1: #H <H %1 %1 normalize
+                       @Exists_append_r @(Exists_add ?? (nil ?))
+                       @Exists_append_r @Exists_append_r
+                       whd %1 //
                      | 2: * ]
               ]
-| 28: whd %1 %1 normalize /2/
-| 29: whd %1 %1 normalize
-      @Exists_append_r @(Exists_add ?? (nil ?)) @Exists_append_r @Exists_append_r 
-      whd %1 //
-| 32: whd %1 %2 whd @(ex_intro … l) @E
+| whd %1 %1 normalize
+  @Exists_append_r @(Exists_add ?? (nil ?)) @Exists_append_r @Exists_append_r 
+  whd %1 //
+| whd %2 %2 whd /2/
+| whd %2 whd /2/
+| whd %1 %2 whd @(ex_intro … l) @E
 ] qed.
 
 axiom ParamGlobalMixup : String.