Finish CondElim proof and fix Gible semantics

3 files changed, 246 insertions, 134 deletions

diff --git a/src/hls/CondElimproof.v b/src/hls/CondElimproof.v
index 8b2ce48..4369d5a 100644
--- a/src/hls/CondElimproof.v
+++ b/src/hls/CondElimproof.v
@@ -101,10 +101,31 @@ Variant match_ps : positive -> predset -> predset -> Prop :=
     (forall x, x <= m -> ps !! x = ps' !! x) ->
     match_ps m ps ps'.
 
+Lemma match_ps_eval_pred :
+  forall p v ps tps b,
+    eval_predf ps p = b ->
+    match_ps v ps tps ->
+    Forall (fun p => p <= v) (predicate_use p) ->
+    eval_predf tps p = b.
+Proof.
+  induction p; crush.
+  - repeat destruct_match. inv H1.
+    unfold eval_predf; simpl.
+    inv H0. rewrite H. eauto. rewrite Pos2Nat.id; auto.
+  - apply Forall_app in H1; inv H1.
+    rewrite ! eval_predf_Pand.
+    erewrite IHp1; eauto.
+    erewrite IHp2; eauto.
+  - apply Forall_app in H1; inv H1.
+    rewrite ! eval_predf_Por.
+    erewrite IHp1; eauto.
+    erewrite IHp2; eauto.
+Qed.
+
 Lemma eval_pred_under_match:
   forall rs m rs' m' ps tps tps' ps' v p1 rs'' ps'' m'',
     eval_pred (Some p1) (mki rs ps m) (mki rs' ps' m') (mki rs'' ps'' m'') ->
-    (forall p, In p (predicate_use p1) -> p <= v) ->
+    Forall (fun p => p <= v) (predicate_use p1) ->
     match_ps v ps tps ->
     match_ps v ps' tps' ->
     exists tps'',
@@ -112,7 +133,11 @@ Lemma eval_pred_under_match:
       /\ match_ps v ps'' tps''.
 Proof.
   inversion 1; subst; simplify.
-    Admitted.
+  econstructor. econstructor. econstructor. simpl.
+  eapply match_ps_eval_pred; eauto. eauto.
+  econstructor. econstructor. econstructor. simpl.
+  eapply match_ps_eval_pred; eauto. eauto.
+Qed.
 
 Lemma eval_pred_eq_predset :
   forall p rs ps m rs' m' ps' rs'' m'',
@@ -132,38 +157,82 @@ Proof.
     eapply in_app_or in H. inv H; eauto.
 Qed.
 
+Lemma truthy_match_ps :
+  forall v ps tps p,
+    truthy ps p ->
+    (forall p', p = Some p' -> Forall (fun x => x <= v) (predicate_use p')) ->
+    match_ps v ps tps ->
+    truthy tps p.
+Proof.
+  inversion 1; crush.
+  constructor.
+  constructor. symmetry in H1. eapply match_ps_eval_pred; eauto.
+Qed.
+
+Lemma instr_falsy_match_ps :
+  forall v ps tps i,
+    instr_falsy ps i ->
+    Forall (fun x => x <= v) (pred_uses i) ->
+    match_ps v ps tps ->
+    instr_falsy tps i.
+Proof.
+  inversion 1; crush; constructor; eapply match_ps_eval_pred; eauto.
+  inv H2; auto.
+Qed.
+
+Ltac truthy_falsy :=
+  match goal with
+  | H1: truthy _ _, H2: instr_falsy _ _ |- _ => inv H1; inv H2; solve [crush]
+  end.
+
 Lemma elim_cond_s_spec :
   forall A B ge sp rs m rs' m' ps tps ps' p a p0 l v,
     step_instr ge sp (Iexec (mki rs ps m)) a (Iexec (mki rs' ps' m')) ->
-    (forall p, In p (pred_uses a) -> p <= v) ->
+    Forall (fun p => p <= v) (pred_uses a) ->
     match_ps v ps tps ->
     elim_cond_s p a = (p0, l) ->
     exists tps',
       step_list2 (@step_instr A B ge) sp (Iexec (mki rs tps m)) l (Iexec (mki rs' tps' m'))
       /\ match_ps v ps' tps'.
 Proof.
-  inversion 1; subst; simplify; inv H.
+  inversion 1; subst; simplify.
   - inv H2. econstructor. split; eauto; econstructor; econstructor.
-  - inv H2. destruct p1.
-    + exploit eval_pred_under_match; eauto; try lia; simplify.
-      econstructor. split. econstructor. econstructor; eauto. eauto. econstructor.
-      eauto.
-    + inv H15. econstructor. split. econstructor. econstructor. eauto. constructor; eauto.
-      constructor. auto.
-  - inv H2. destruct p1.
-    + exploit eval_pred_under_match; eauto; try lia; simplify.
-      econstructor. split. econstructor. econstructor; eauto.
-      constructor. eauto.
-    + inv H18. econstructor. split. econstructor. econstructor; eauto. constructor; eauto.
-      constructor. auto.
-  - inv H2. destruct p1.
-    + exploit eval_pred_under_match; eauto; try lia; simplify.
-      econstructor. split. econstructor. econstructor; eauto.
-      constructor. auto.
-    + inv H18. econstructor. split. econstructor. econstructor; eauto. constructor; eauto.
-      constructor. auto.
-  - inv H2. destruct p'.
-    exploit eval_pred_under_match; eauto. Admitted.
+  - inv H2. do 2 econstructor; eauto. econstructor; eauto.
+    econstructor; eauto. eapply truthy_match_ps; eauto.
+    intros. destruct p1; try discriminate; crush.
+    constructor.
+  - inv H2. do 2 econstructor; eauto. econstructor; eauto.
+    econstructor; eauto. eapply truthy_match_ps; eauto.
+    intros. destruct p1; try discriminate; crush.
+    constructor.
+  - inv H2. do 2 econstructor; eauto. econstructor; eauto.
+    econstructor; eauto. eapply truthy_match_ps; eauto.
+    intros. destruct p1; try discriminate; crush.
+    constructor.
+  - inv H2. do 2 econstructor; eauto. econstructor; eauto.
+    econstructor; eauto. eapply truthy_match_ps; eauto.
+    intros. destruct p'; try discriminate; crush. inv H0; auto.
+    constructor.
+    constructor; intros.
+    destruct (peq x p1); subst.
+    { rewrite ! PMap.gss; auto. }
+    { inv H1. rewrite ! PMap.gso; auto. }
+  - do 2 econstructor; eauto.
+    unfold elim_cond_s in H2.
+    destruct a; inv H2;
+      try (econstructor;
+           [eapply exec_RB_falsy; simplify; eapply instr_falsy_match_ps; eauto|constructor]).
+    destruct c; inv H5;
+      try (econstructor;
+           [eapply exec_RB_falsy; simplify; eapply instr_falsy_match_ps; eauto|constructor]).
+    inv H4.
+    econstructor. eapply exec_RB_falsy. econstructor. eapply match_ps_eval_pred; eauto.
+    econstructor. eapply exec_RB_falsy. econstructor. simplify.
+    rewrite eval_predf_Pand. apply andb_false_intro2. eapply match_ps_eval_pred; eauto.
+    econstructor. eapply exec_RB_falsy. econstructor. simplify.
+    rewrite eval_predf_Pand. apply andb_false_intro2. eapply match_ps_eval_pred; eauto.
+    constructor.
+Qed.
 
 Definition wf_predicate (v: predicate) (p: predicate) := v < p.
 
@@ -172,7 +241,19 @@ Lemma eval_predf_match_ps :
     match_ps v p p' ->
     Forall (fun x => x <= v) (predicate_use p0) ->
     eval_predf p p0 = eval_predf p' p0.
-  Admitted.
+Proof.
+  induction p0; crush.
+  - unfold eval_predf. simplify. destruct p0.
+    rewrite Pos2Nat.id. inv H. inv H0. rewrite H1; auto.
+  - eapply Forall_app in H0. inv H0.
+    rewrite ! eval_predf_Pand.
+    erewrite IHp0_1; eauto.
+    erewrite IHp0_2; eauto.
+  - eapply Forall_app in H0. inv H0.
+    rewrite ! eval_predf_Por.
+    erewrite IHp0_1; eauto.
+    erewrite IHp0_2; eauto.
+Qed.
 
 Lemma step_cf_instr_ps_const :
   forall ge stk f sp pc rs' ps' m' cf t pc' rs'' ps'' m'',
@@ -217,9 +298,7 @@ Lemma step_instr_inv_exit :
     @step_instr A B ge sp (Iexec i) (RBexit (Some p) cf) (Iterm i cf).
 Proof.
   intros.
-  replace (Iterm i cf) with (if (eval_predf (is_ps i) p) then Iterm i cf else Iexec i).
-  constructor; auto.
-  rewrite H; auto.
+  econstructor. constructor; eauto.
 Qed.
 
 Lemma step_instr_inv_exit2 :
@@ -228,29 +307,62 @@ Lemma step_instr_inv_exit2 :
     @step_instr A B ge sp (Iexec i) (RBexit (Some p) cf) (Iexec i).
 Proof.
   intros.
-  replace (Iexec i) with (if (eval_predf (is_ps i) p) then Iterm i cf else Iexec i) at 2.
-  constructor; auto.
-  rewrite H; auto.
+  eapply exec_RB_falsy; constructor; auto.
+Qed.
+
+Lemma eval_predf_set_gt:
+  forall p1 v ps b p tps,
+    eval_predf ps p1 = true ->
+    Forall (fun x : positive => x <= v) (predicate_use p1) ->
+    wf_predicate v p -> match_ps v ps tps -> eval_predf tps # p <- b p1 = true.
+Proof.
+  induction p1; crush.
+  - unfold eval_predf. simplify. destruct p. rewrite Pos2Nat.id.
+    assert (p <> p0).
+    { inv H0. unfold wf_predicate in H1. lia. }
+    rewrite ! PMap.gso by auto. inv H2.
+    inv H0. rewrite <- H4 by auto. unfold eval_predf in H.
+    simplify. rewrite Pos2Nat.id in H. auto.
+  - rewrite eval_predf_Pand. apply Forall_app in H0.
+    rewrite eval_predf_Pand in H. apply andb_true_iff in H.
+    apply andb_true_iff; simplify.
+    eauto.
+    eauto.
+  - rewrite eval_predf_Por. apply Forall_app in H0.
+    rewrite eval_predf_Por in H. apply orb_true_iff in H.
+    apply orb_true_iff; simplify. inv H; eauto.
 Qed.
 
 Lemma eval_predf_in_ps :
-  forall v ps ps' p1 b p tps,
+  forall v ps p1 b p tps,
     eval_predf ps p1 = true ->
     Forall (fun x => x <= v) (predicate_use p1) ->
     wf_predicate v p ->
-    match_ps v ps ps' ->
+    match_ps v ps tps ->
     eval_predf tps # p <- b (Pand (Plit (b, p)) p1) = true.
-Admitted.
+Proof.
+  intros.
+  rewrite eval_predf_Pand. apply andb_true_iff. split.
+  unfold eval_predf. simplify. rewrite Pos2Nat.id.
+  rewrite PMap.gss. destruct b; auto.
+  eapply eval_predf_set_gt; eauto.
+Qed.
 
 Lemma eval_predf_in_ps2 :
-  forall v ps ps' p1 b b' p tps,
+  forall v ps p1 b b' p tps,
     eval_predf ps p1 = true ->
     Forall (fun x => x <= v) (predicate_use p1) ->
     wf_predicate v p ->
-    match_ps v ps ps' ->
+    match_ps v ps tps ->
     b <> b' ->
     eval_predf tps # p <- b (Pand (Plit (b', p)) p1) = false.
-Admitted.
+Proof.
+  intros.
+  rewrite eval_predf_Pand. apply andb_false_iff.
+  unfold eval_predf. simplify. left.
+  rewrite Pos2Nat.id. rewrite PMap.gss.
+  now destruct b, b'.
+Qed.
 
 Lemma match_ps_set_gt :
   forall v ps tps p b,
@@ -474,54 +586,37 @@ Section CORRECTNESS.
         /\ match_states st st'.
   Proof using TRANSL.
     inversion 1; subst; simplify.
-    - destruct (eval_predf ps p1) eqn:?; [|discriminate]. inv H2.
-      destruct cf; inv H5;
-        try (exploit step_cf_instr_ge; eauto; econstructor; eauto; simplify;
-             do 3 econstructor; simplify;
-             [ constructor; apply step_instr_inv_exit; erewrite <- eval_predf_match_ps | | | ]);
-        eauto using step_cf_instr_ps_idem.
-      inv H0; destruct b.
-      + do 3 econstructor; simplify.
-        econstructor. econstructor; eauto. eapply eval_pred_true.
-        erewrite <- eval_predf_match_ps; eauto. simpl.
-        constructor. apply step_instr_inv_exit. simpl.
-        eapply eval_predf_in_ps; eauto.
-        apply match_ps_set_gt; auto.
-        constructor; auto.
-        constructor; auto.
-        apply match_ps_set_gt; auto.
-      + do 3 econstructor; simplify.
-        econstructor. econstructor; eauto. eapply eval_pred_true.
-        erewrite <- eval_predf_match_ps; eauto.
-        econstructor. apply step_instr_inv_exit2. simpl.
-        eapply eval_predf_in_ps2; eauto.
-        constructor. apply step_instr_inv_exit. simpl.
-        eapply eval_predf_in_ps; eauto.
-        apply match_ps_set_gt; auto.
-        constructor; auto.
-        constructor; auto.
-        apply match_ps_set_gt; auto.
-    - destruct cf; inv H4; exploit step_cf_instr_ge; eauto; try solve [econstructor; eauto]; simplify;
-        try (do 3 econstructor; simplify; eauto; eapply exec_RBterm; econstructor; eauto).
-      inv H0. destruct b.
-      + do 3 econstructor; simplify.
-        econstructor. econstructor; eauto. constructor.
-        constructor. apply step_instr_inv_exit. simplify.
-        unfold eval_predf. simplify. rewrite Pos2Nat.id. apply PMap.gss.
-        apply match_ps_set_gt; auto.
-        constructor; auto.
-        constructor; auto.
-        apply match_ps_set_gt; auto.
-      + do 3 econstructor; simplify.
-        econstructor. econstructor; eauto. constructor.
-        econstructor. apply step_instr_inv_exit2. simpl.
-        unfold eval_predf. simplify. rewrite Pos2Nat.id. apply PMap.gss.
-        constructor. apply step_instr_inv_exit. simpl.
-        unfold eval_predf. simplify. rewrite Pos2Nat.id. rewrite PMap.gss. auto.
-        apply match_ps_set_gt; auto.
-        constructor; auto.
-        constructor; auto.
-        apply match_ps_set_gt; auto.
+    destruct cf;
+      try (inv H5; exploit step_cf_instr_ge; eauto; [econstructor|]; eauto; simplify;
+           do 3 econstructor; simplify; eauto;
+           constructor; constructor; eapply truthy_match_ps; eauto;
+           intros; match goal with H: _ = Some _ |- _ => inv H end; auto).
+    inv H0; destruct b.
+    + inv H5; do 3 econstructor; simplify.
+      econstructor. econstructor; eauto.
+      eapply truthy_match_ps; eauto; intros; match goal with H: _ = Some _ |- _ => inv H end; auto.
+      constructor.
+      econstructor. simplify. destruct p1.
+      constructor. inv H4. eapply eval_predf_in_ps; eauto.
+      constructor. unfold eval_predf; simplify. rewrite Pos2Nat.id.
+      apply PMap.gss.
+      apply match_ps_set_gt; auto.
+      constructor; auto.
+      constructor; auto.
+      apply match_ps_set_gt; auto.
+    + inv H5; do 3 econstructor; simplify.
+      econstructor. econstructor; eauto.
+      eapply truthy_match_ps; eauto; intros; match goal with H: _ = Some _ |- _ => inv H end; auto.
+      econstructor. eapply exec_RB_falsy. simplify. destruct p1.
+      constructor. inv H4. eapply eval_predf_in_ps2; eauto.
+      constructor. unfold eval_predf; simplify. rewrite Pos2Nat.id. apply PMap.gss.
+      constructor. econstructor. inv H4. constructor. unfold eval_predf; simplify.
+      rewrite Pos2Nat.id. rewrite PMap.gss. auto.
+      constructor. eapply eval_predf_in_ps; eauto.
+      apply match_ps_set_gt; auto.
+      constructor; auto.
+      constructor; auto.
+      apply match_ps_set_gt; auto.
   Qed.
 
   Lemma replace_section_spec :
@@ -541,7 +636,7 @@ Section CORRECTNESS.
   Proof using TRANSL.
     induction bb; simplify; inv H.
     - destruct state'. repeat destruct_match. inv H4.
-      exploit elim_cond_s_spec; eauto. simplify.
+      exploit elim_cond_s_spec; eauto. apply Forall_forall. intros; eauto. simplify.
       exploit IHbb; eauto; simplify.
       do 3 econstructor. simplify.
       eapply append. econstructor; simplify.
@@ -567,24 +662,6 @@ Section CORRECTNESS.
       c ! pc = Some bb ->
       max_pred_block 1 n bb <= m.
 
-  (* Lemma max_pred_block_lt: *)
-  (*   forall v v0 n b k, *)
-  (*     v0 <= b -> *)
-  (*     max_pred_block v0 n v <= max_pred_block b k v. *)
-  (*   Proof. Admitted. *)
-
-  (* Lemma max_block_pred : *)
-  (*   forall f, lt_pred f.(fn_code) (max_pred_function f). *)
-  (* Proof. *)
-  (*   unfold max_pred_function; intros. *)
-  (*   eapply PTree_Properties.fold_ind; unfold lt_pred; intros. *)
-  (*   destruct (max_pred_block 1 n bb); crush. *)
-  (*   destruct (peq pc k); subst; simplify. *)
-  (*   - assert (v0 <= a \/ a < v0) by admit. *)
-  (*     inv H3. left. eapply max_pred_block_lt; eauto. *)
-  (*     right. *)
-  (*     Abort. *)
-
   Lemma elim_cond_s_lt :
     forall p a p0 l x,
       elim_cond_s p a = (p0, l) ->
diff --git a/src/hls/Gible.v b/src/hls/Gible.v
index c51b250..4cecd2c 100644
--- a/src/hls/Gible.v
+++ b/src/hls/Gible.v
@@ -241,46 +241,77 @@ Step Instruction
 =============================
 |*)
 
+Definition truthyb (ps: predset) (p: option pred_op) :=
+  match p with
+  | None => true
+  | Some p' => eval_predf ps p'
+  end.
+
+Variant truthy (ps: predset): option pred_op -> Prop :=
+  | truthy_None: truthy ps None
+  | truthy_Some: forall p, eval_predf ps p = true -> truthy ps (Some p).
+
+Variant instr_falsy (ps: predset): instr -> Prop :=
+  | RBop_falsy :
+    forall p op args res,
+      eval_predf ps p = false ->
+      instr_falsy ps (RBop (Some p) op args res)
+  | RBload_falsy:
+    forall p chunk addr args dst,
+      eval_predf ps p = false ->
+      instr_falsy ps (RBload (Some p) chunk addr args dst)
+  | RBstore_falsy:
+    forall p chunk addr args src,
+      eval_predf ps p = false ->
+      instr_falsy ps (RBstore (Some p) chunk addr args src)
+  | RBsetpred_falsy:
+    forall p c args pred,
+      eval_predf ps p = false ->
+      instr_falsy ps (RBsetpred (Some p) c args pred)
+  | RBexit_falsy:
+    forall p cf,
+      eval_predf ps p = false ->
+      instr_falsy ps (RBexit (Some p) cf)
+  .
+
 Variant step_instr: val -> istate -> instr -> istate -> Prop :=
   | exec_RBnop:
     forall sp ist,
       step_instr sp (Iexec ist) RBnop (Iexec ist)
   | exec_RBop:
-    forall op v res args rs m sp p ist pr,
+    forall op v res args rs m sp p pr,
       eval_operation ge sp op rs##args m = Some v ->
-      eval_pred p (mk_instr_state rs pr m)
-                (mk_instr_state (rs#res <- v) pr m) ist ->
-      step_instr sp (Iexec (mk_instr_state rs pr m)) (RBop p op args res) (Iexec ist)
+      truthy pr p ->
+      step_instr sp (Iexec (mk_instr_state rs pr m)) (RBop p op args res)
+                 (Iexec (mk_instr_state (rs#res <- v) pr m))
   | exec_RBload:
-    forall addr rs args a chunk m v dst sp p pr ist,
+    forall addr rs args a chunk m v dst sp p pr,
       eval_addressing ge sp addr rs##args = Some a ->
       Mem.loadv chunk m a = Some v ->
-      eval_pred p (mk_instr_state rs pr m)
-                (mk_instr_state (rs#dst <- v) pr m) ist ->
+      truthy pr p ->
       step_instr sp (Iexec (mk_instr_state rs pr m))
-                 (RBload p chunk addr args dst) (Iexec ist)
+                 (RBload p chunk addr args dst) (Iexec (mk_instr_state (rs#dst <- v) pr m))
   | exec_RBstore:
-    forall addr rs args a chunk m src m' sp p pr ist,
+    forall addr rs args a chunk m src m' sp p pr,
       eval_addressing ge sp addr rs##args = Some a ->
       Mem.storev chunk m a rs#src = Some m' ->
-      eval_pred p (mk_instr_state rs pr m)
-                (mk_instr_state rs pr m') ist ->
+      truthy pr p ->
       step_instr sp (Iexec (mk_instr_state rs pr m))
-                 (RBstore p chunk addr args src) (Iexec ist)
+                 (RBstore p chunk addr args src) (Iexec (mk_instr_state rs pr m'))
   | exec_RBsetpred:
-    forall sp rs pr m p c b args p' ist,
+    forall sp rs pr m p c b args p',
       Op.eval_condition c rs##args m = Some b ->
-      eval_pred p' (mk_instr_state rs pr m)
-                (mk_instr_state rs (pr#p <- b) m) ist ->
+      truthy pr p' ->
       step_instr sp (Iexec (mk_instr_state rs pr m))
-                 (RBsetpred p' c args p) (Iexec ist)
-  | exec_RBexit_Some:
-    forall p c sp b i,
-      eval_predf (is_ps i) p = b ->
-      step_instr sp (Iexec i) (RBexit (Some p) c) (if b then Iterm i c else Iexec i)
-  | exec_RBexit_None:
-    forall c sp i,
-      step_instr sp (Iexec i) (RBexit None c) (Iterm i c)
+                 (RBsetpred p' c args p) (Iexec (mk_instr_state rs (pr#p <- b) m))
+  | exec_RBexit:
+    forall p c sp i,
+      truthy (is_ps i) p ->
+      step_instr sp (Iexec i) (RBexit p c) (Iterm i c)
+  | exec_RB_falsy :
+    forall sp st i,
+      instr_falsy (is_ps st) i ->
+      step_instr sp (Iexec st) i (Iexec st)
 .
 
 End RELABSTR.
diff --git a/src/hls/GibleSeqgenproof.v b/src/hls/GibleSeqgenproof.v
index feaa346..fd336ed 100644
--- a/src/hls/GibleSeqgenproof.v
+++ b/src/hls/GibleSeqgenproof.v
@@ -462,6 +462,7 @@ whole execution (in one big step) of the basic block.
       eassumption.
       eapply BB; [| eassumption ].
       econstructor. econstructor. eapply exec_RBterm. econstructor.
+      constructor.
       econstructor.
 
       econstructor; try eassumption. eauto.
@@ -552,6 +553,7 @@ whole execution (in one big step) of the basic block.
     eapply BB; [| eassumption ]. econstructor. econstructor.
     rewrite <- eval_op_eq; eassumption. constructor.
     eapply exec_RBterm. econstructor. econstructor.
+    constructor.
 
     econstructor; try eassumption. eauto.
     eapply star_refl.
@@ -615,6 +617,7 @@ whole execution (in one big step) of the basic block.
       eapply BB; [| eassumption ]. econstructor. econstructor; eauto.
       rewrite <- eval_addressing_eq; eassumption. constructor.
       eapply exec_RBterm. econstructor. econstructor.
+      constructor.
 
       econstructor; try eassumption. eauto.
       eapply star_refl.
@@ -661,6 +664,7 @@ whole execution (in one big step) of the basic block.
       eapply BB; [| eassumption ]. econstructor. econstructor; eauto.
       rewrite <- eval_addressing_eq; eassumption. constructor.
       eapply exec_RBterm. econstructor. econstructor.
+      constructor.
 
       econstructor; try eassumption. eauto.
       eapply star_refl.
@@ -723,7 +727,7 @@ whole execution (in one big step) of the basic block.
     eassumption.
 
     eapply BB; [| eassumption ]. econstructor. econstructor; eauto.
-    constructor. econstructor; eauto. econstructor; eauto.
+    constructor. econstructor; eauto. constructor. econstructor; eauto.
     apply sig_transl_function; auto.
 
     econstructor; try eassumption.
@@ -755,7 +759,7 @@ whole execution (in one big step) of the basic block.
     eassumption.
 
     eapply BB; [| eassumption ]. econstructor. econstructor; eauto.
-    constructor. econstructor; eauto. econstructor; eauto.
+    constructor. econstructor; eauto. constructor. econstructor; eauto.
     apply sig_transl_function; auto.
 
     assert (fn_stacksize tf = RTL.fn_stacksize f).
@@ -788,7 +792,7 @@ whole execution (in one big step) of the basic block.
     eassumption.
 
     eapply BB; [| eassumption ]. econstructor. econstructor; eauto.
-    constructor. econstructor; eauto. econstructor; eauto.
+    constructor. econstructor; eauto. constructor. econstructor; eauto.
     eauto using eval_builtin_args_preserved, symbols_preserved.
     eauto using external_call_symbols_preserved, senv_preserved.
 
@@ -904,7 +908,7 @@ whole execution (in one big step) of the basic block.
       econstructor; eauto.
 
       eapply BB. econstructor. econstructor.
-      eapply exec_RBterm. econstructor; eauto. assumption.
+      eapply exec_RBterm. econstructor; eauto. constructor. assumption.
       econstructor; eauto.
       constructor; eauto using star_refl.
       unfold sem_extrap; intros. setoid_rewrite H4 in H6. inv H6. auto.
@@ -912,7 +916,7 @@ whole execution (in one big step) of the basic block.
     { do 3 econstructor. apply plus_one.
       econstructor; eauto.
       eapply BB. econstructor. econstructor.
-      eapply exec_RBterm. econstructor; eauto. assumption.
+      eapply exec_RBterm. econstructor; eauto. constructor. assumption.
       econstructor; eauto.
       constructor; eauto using star_refl.
       unfold sem_extrap; intros. setoid_rewrite H0 in H6. inv H6. auto.
@@ -940,7 +944,7 @@ whole execution (in one big step) of the basic block.
     do 3 econstructor. apply plus_one.
     econstructor; eauto. eapply BB.
     econstructor. econstructor. eapply exec_RBterm.
-    econstructor. assumption.
+    econstructor. constructor. assumption.
     econstructor; eauto.
 
     constructor; eauto using star_refl.
@@ -969,7 +973,7 @@ whole execution (in one big step) of the basic block.
     do 3 econstructor. apply plus_one. econstructor; eauto.
     eapply BB.
     econstructor. econstructor. eapply exec_RBterm.
-    econstructor. eauto.
+    econstructor. constructor. eauto.
     econstructor; eauto.
     rewrite H4. eauto.
     constructor; eauto.