Add new block generation for Gible

6 files changed, 298 insertions, 457 deletions

diff --git a/src/Compiler.v b/src/Compiler.v
index d6d87e2..dc3b1c7 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -60,8 +60,8 @@ Require vericert.hls.Verilog.
 Require vericert.hls.Veriloggen.
 Require vericert.hls.Veriloggenproof.
 Require vericert.hls.HTLgen.
-Require vericert.hls.RTLBlock.
-Require vericert.hls.RTLBlockgen.
+Require vericert.hls.GibleSeq.
+Require vericert.hls.GibleSeqgen.
 Require vericert.hls.RTLPargen.
 Require vericert.hls.RTLParFUgen.
 Require vericert.hls.HTLPargen.
diff --git a/src/common/DecEq.v b/src/common/DecEq.v
index e9d716f..5f85e9b 100644
--- a/src/common/DecEq.v
+++ b/src/common/DecEq.v
@@ -28,8 +28,7 @@ Require Import compcert.lib.Integers.
 Require Import compcert.lib.Floats.
 
 Require Import vericert.common.Vericertlib.
-Require Import vericert.hls.RTLBlockInstr.
-Require Import vericert.hls.RTLBlock.
+Require Import vericert.hls.Gible.
 
 Lemma comparison_eq: forall (x y : comparison), {x = y} + {x <> y}.
 Proof.
@@ -115,6 +114,10 @@ Proof.
   generalize Pos.eq_dec; intro.
   generalize typ_eq; intro.
   generalize Int.eq_dec; intro.
+  generalize Ptrofs.eq_dec; intro.
+  generalize Int64.eq_dec; intro.
+  generalize Float.eq_dec; intro.
+  generalize Float32.eq_dec; intro.
   generalize memory_chunk_eq; intro.
   generalize addressing_eq; intro.
   generalize operation_eq; intro.
diff --git a/src/hls/GibleSeq.v b/src/hls/GibleSeq.v
index 321d639..1ba28bc 100644
--- a/src/hls/GibleSeq.v
+++ b/src/hls/GibleSeq.v
@@ -68,3 +68,4 @@ function that can execute lists of things, given their execution rule.
 End BB.
 
 Module GibleSeq := Gible(BB).
+Export GibleSeq.
diff --git a/src/hls/GibleSeqgen.v b/src/hls/GibleSeqgen.v
new file mode 100644
index 0000000..8d52339
--- /dev/null
+++ b/src/hls/GibleSeqgen.v
@@ -0,0 +1,153 @@
+(*|
+..
+   Vericert: Verified high-level synthesis.
+   Copyright (C) 2020-2022 Yann Herklotz <yann@yannherklotz.com>
+
+   This program is free software: you can redistribute it and/or modify
+   it under the terms of the GNU General Public License as published by
+   the Free Software Foundation, either version 3 of the License, or
+   (at your option) any later version.
+
+   This program is distributed in the hope that it will be useful,
+   but WITHOUT ANY WARRANTY; without even the implied warranty of
+   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+   GNU General Public License for more details.
+
+   You should have received a copy of the GNU General Public License
+   along with this program.  If not, see <https://www.gnu.org/licenses/>.
+
+===========
+RTLBlockgen
+===========
+
+.. coq:: none
+|*)
+
+Require compcert.backend.RTL.
+Require Import compcert.common.AST.
+Require Import compcert.lib.Maps.
+Require Import compcert.lib.Integers.
+Require Import compcert.lib.Floats.
+
+Require Import vericert.common.DecEq.
+Require Import vericert.common.Vericertlib.
+Require Import vericert.hls.Gible.
+Require Import vericert.hls.GibleSeq.
+
+#[local] Open Scope positive.
+
+Definition check_valid_node (tc: code) (e: node) :=
+  match tc ! e with
+  | Some _ => true
+  | _ => false
+  end.
+
+Fixpoint check_code (c: RTL.code) (tc: code) (pc: node) (b: BB.t) :=
+  match c ! pc, b with
+  | Some (RTL.Inop pc'), RBnop :: (_ :: _ :: _) as b' =>
+      check_code c tc pc' b'
+  | Some (RTL.Iop op' args' dst' pc'), RBop None op args dst :: (_ :: _ :: _) as b' =>
+      ceq operation_eq op op'
+      && ceq list_pos_eq args args'
+      && ceq peq dst dst'
+      && check_code c tc pc' b'
+  | Some (RTL.Iload chunk' addr' args' dst' pc'),
+    RBload None chunk addr args dst :: (_ :: _ :: _) as b' =>
+      ceq memory_chunk_eq chunk chunk'
+      && ceq addressing_eq addr addr'
+      && ceq list_pos_eq args args'
+      && ceq peq dst dst'
+      && check_code c tc pc' b'
+  | Some (RTL.Istore chunk' addr' args' src' pc'),
+    RBstore None chunk addr args src :: (_ :: _ :: _) as b' =>
+      ceq memory_chunk_eq chunk chunk'
+      && ceq addressing_eq addr addr'
+      && ceq list_pos_eq args args'
+      && ceq peq src src'
+      && check_code c tc pc' b'
+  | Some (RTL.Inop pc''), RBnop :: RBexit None (RBgoto pc') :: nil =>
+      check_valid_node tc pc'
+      && ceq peq pc' pc''
+  | Some (RTL.Iop op' args' dst' pc''), RBop None op args dst :: RBexit None (RBgoto pc') :: nil =>
+      check_valid_node tc pc'
+      && ceq peq pc' pc''
+      && ceq operation_eq op op'
+      && ceq list_pos_eq args args'
+      && ceq peq dst dst'
+  | Some (RTL.Iload chunk' addr' args' dst' pc''),
+    RBload None chunk addr args dst :: RBexit None (RBgoto pc') :: nil =>
+      check_valid_node tc pc'
+      && ceq peq pc' pc''
+      && ceq memory_chunk_eq chunk chunk'
+      && ceq addressing_eq addr addr'
+      && ceq list_pos_eq args args'
+      && ceq peq dst dst'
+  | Some (RTL.Istore chunk' addr' args' src' pc''),
+    RBstore None chunk addr args src :: RBexit None (RBgoto pc') :: nil =>
+      check_valid_node tc pc'
+      && ceq peq pc' pc''
+      && ceq memory_chunk_eq chunk chunk'
+      && ceq addressing_eq addr addr'
+      && ceq list_pos_eq args args'
+      && ceq peq src src'
+  | Some (RTL.Icall sig' (inl r') args' dst' pc''),
+    RBnop :: RBexit None (RBcall sig (inl r) args dst pc') :: nil =>
+      check_valid_node tc pc'
+      && ceq peq pc' pc''
+      && ceq signature_eq sig sig'
+      && ceq peq r r'
+      && ceq list_pos_eq args args'
+      && ceq peq dst dst'
+  | Some (RTL.Icall sig' (inr i') args' dst' pc''),
+    RBnop :: RBexit None (RBcall sig (inr i) args dst pc') :: nil =>
+      check_valid_node tc pc'
+      && ceq peq pc' pc''
+      && ceq signature_eq sig sig'
+      && ceq peq i i'
+      && ceq list_pos_eq args args'
+      && ceq peq dst dst'
+  | Some (RTL.Itailcall sig (inl r) args),
+    RBnop :: RBexit None (RBtailcall sig' (inl r') args') :: nil =>
+      ceq signature_eq sig sig'
+      && ceq peq r r'
+      && ceq list_pos_eq args args'
+  | Some (RTL.Itailcall sig (inr r) args),
+    RBnop :: RBexit None (RBtailcall sig' (inr r') args') :: nil =>
+      ceq signature_eq sig sig'
+      && ceq peq r r'
+      && ceq list_pos_eq args args'
+  | Some (RTL.Icond cond args n1 n2), RBnop :: RBexit None (RBcond cond' args' n1' n2') :: nil =>
+      check_valid_node tc n1
+      && check_valid_node tc n2
+      && ceq condition_eq cond cond'
+      && ceq list_pos_eq args args'
+      && ceq peq n1 n1'
+      && ceq peq n2 n2'
+  | Some (RTL.Ijumptable r ns), RBnop :: RBexit None (RBjumptable r' ns') :: nil =>
+      ceq peq r r'
+      && ceq list_pos_eq ns ns'
+      && forallb (check_valid_node tc) ns
+  | Some (RTL.Ireturn (Some r)), RBnop :: RBexit None (RBreturn (Some r')) :: nil =>
+      ceq peq r r'
+  | Some (RTL.Ireturn None), RBnop :: RBexit None (RBreturn None) :: nil => true
+  | _, _ => false
+  end.
+
+Parameter partition : RTL.function -> Errors.res function.
+
+Definition transl_function (f: RTL.function) :=
+  match partition f with
+  | Errors.OK f' =>
+      if check_valid_node f'.(fn_code) f.(RTL.fn_entrypoint) then
+        if forall_ptree (check_code f.(RTL.fn_code) f'.(fn_code)) f'.(fn_code) then
+          Errors.OK
+            (mkfunction f.(RTL.fn_sig) f.(RTL.fn_params) f.(RTL.fn_stacksize) f'.(fn_code) f.(RTL.fn_entrypoint))
+        else Errors.Error (Errors.msg "check_present_blocks failed")
+      else Errors.Error (Errors.msg "entrypoint does not exists")
+  | Errors.Error msg => Errors.Error msg
+  end.
+
+Definition transl_fundef := transf_partial_fundef transl_function.
+
+Definition transl_program : RTL.program -> Errors.res program :=
+  transform_partial_program transl_fundef.
diff --git a/src/hls/RTLBlockgenproof.v b/src/hls/GibleSeqgenproof.v
index 642264f..55b25d1 100644
--- a/src/hls/RTLBlockgenproof.v
+++ b/src/hls/GibleSeqgenproof.v
@@ -36,9 +36,9 @@ Require Import compcert.common.Values.
 
 Require Import vericert.common.Vericertlib.
 Require Import vericert.common.DecEq.
-Require Import vericert.hls.RTLBlockInstr.
-Require Import vericert.hls.RTLBlock.
-Require Import vericert.hls.RTLBlockgen.
+Require Import vericert.hls.Gible.
+Require Import vericert.hls.GibleSeq.
+Require Import vericert.hls.GibleSeqgen.
 
 #[local] Open Scope positive.
 
@@ -73,49 +73,12 @@ cases are similar enough that they can be merged into one.
 Definition all_max {A} (c: PTree.t A) p: Prop :=
   Forall (fun x => x <= p) (map fst (PTree.elements c)).
 
-Definition find_block_spec (c: code) (n1 n2: node): Prop :=
-  forall x, all_max c x -> find_block x (map fst (PTree.elements c)) n1 = n2.
-
 Definition offset (pc pc': positive): nat := Pos.to_nat pc' - Pos.to_nat pc.
 
-Definition find_instr_spec (c: code) (n: node) (i: RTL.instruction)
-           (n': node) (i': instr) :=
-  find_block_spec c n n' /\
-  exists il, c ! n' = Some il
-        /\ nth_error il.(bb_body) (offset n n') = Some i'.
-
-(*|
-.. index::
-   pair: semantics; transl_code_spec
-
-Translation Specification
--------------------------
-
-This specification should describe the translation that the unverified
-transformation performs.  This should be proven from the validation of the
-transformation.
-
-This also specifies ``x'`` relative to x given the code.
-|*)
-
-Variant transl_code_spec (c: RTL.code) (tc: code) (x x': node) (i: RTL.instruction) (i': instr): Prop :=
-| transl_code_standard_bb :
-    c ! x = Some i ->
-    Is_true (check_instr x i i') ->
-    transl_code_spec c tc x x' i i'
-| transl_code_standard_cf :
-  forall il,
-    c ! x = Some i ->
-    tc ! x' = Some il ->
-    Is_true (check_cf_instr_body i i') ->
-    Is_true (check_cf_instr i il.(bb_exit)) ->
-    transl_code_spec c tc x x' i i'
-.
-
 Section CORRECTNESS.
 
   Context (prog : RTL.program).
-  Context (tprog : RTLBlock.program).
+  Context (tprog : GibleSeq.program).
 
   Let ge : RTL.genv := Globalenvs.Genv.globalenv prog.
   Let tge : genv := Globalenvs.Genv.globalenv tprog.
@@ -141,71 +104,71 @@ finding is actually done at that higher level already.
 
   Definition valid_succ (tc: code) (pc: node) : Prop := exists b, tc ! pc = Some b.
 
-  Inductive match_block (c: RTL.code) (tc: code) (pc: node): bb -> cf_instr -> Prop :=
+  Inductive match_block (c: RTL.code) (tc: code) (pc: node): BB.t -> Prop :=
   (*
    * Basic Block Instructions
    *)
-  | match_block_nop b cf pc':
+  | match_block_nop b pc':
     c ! pc = Some (RTL.Inop pc') ->
-    match_block c tc pc' b cf ->
-    match_block c tc pc (RBnop :: b) cf
-  | match_block_op cf b op args dst pc':
+    match_block c tc pc' b ->
+    match_block c tc pc (RBnop :: b)
+  | match_block_op b op args dst pc':
     c ! pc = Some (RTL.Iop op args dst pc') ->
-    match_block c tc pc' b cf ->
-    match_block c tc pc (RBop None op args dst :: b) cf
-  | match_block_load cf b chunk addr args dst pc':
+    match_block c tc pc' b ->
+    match_block c tc pc (RBop None op args dst :: b)
+  | match_block_load b chunk addr args dst pc':
     c ! pc = Some (RTL.Iload chunk addr args dst pc') ->
-    match_block c tc pc' b cf ->
-    match_block c tc pc (RBload None chunk addr args dst :: b) cf
-  | match_block_store cf b chunk addr args src pc':
+    match_block c tc pc' b ->
+    match_block c tc pc (RBload None chunk addr args dst :: b)
+  | match_block_store b chunk addr args src pc':
     c ! pc = Some (RTL.Istore chunk addr args src pc') ->
-    match_block c tc pc' b cf ->
-    match_block c tc pc (RBstore None chunk addr args src :: b) cf
+    match_block c tc pc' b ->
+    match_block c tc pc (RBstore None chunk addr args src :: b)
   (*
    * Control flow instructions using goto
    *)
   | match_block_goto pc':
     c ! pc = Some (RTL.Inop pc') ->
     valid_succ tc pc' ->
-    match_block c tc pc (RBnop :: nil) (RBgoto pc')
+    match_block c tc pc (RBnop :: RBexit None (RBgoto pc') :: nil)
   | match_block_op_cf pc' op args dst:
     c ! pc = Some (RTL.Iop op args dst pc') ->
     valid_succ tc pc' ->
-    match_block c tc pc (RBop None op args dst :: nil) (RBgoto pc')
+    match_block c tc pc (RBop None op args dst :: RBexit None (RBgoto pc') :: nil)
   | match_block_load_cf pc' chunk addr args dst:
     c ! pc = Some (RTL.Iload chunk addr args dst pc') ->
     valid_succ tc pc' ->
-    match_block c tc pc (RBload None chunk addr args dst :: nil) (RBgoto pc')
+    match_block c tc pc (RBload None chunk addr args dst :: RBexit None (RBgoto pc') :: nil)
   | match_block_store_cf pc' chunk addr args src:
     c ! pc = Some (RTL.Istore chunk addr args src pc') ->
     valid_succ tc pc' ->
-    match_block c tc pc (RBstore None chunk addr args src :: nil) (RBgoto pc')
+    match_block c tc pc (RBstore None chunk addr args src :: RBexit None (RBgoto pc') :: nil)
   (*
    * Standard control flow instructions
    *)
   | match_block_call sig ident args dst pc' :
     c ! pc = Some (RTL.Icall sig ident args dst pc') ->
     valid_succ tc pc' ->
-    match_block c tc pc (RBnop :: nil) (RBcall sig ident args dst pc')
+    match_block c tc pc (RBnop :: RBexit None (RBcall sig ident args dst pc') :: nil)
   | match_block_tailcall sig ident args :
     c ! pc = Some (RTL.Itailcall sig ident args) ->
-    match_block c tc pc (RBnop :: nil) (RBtailcall sig ident args)
+    match_block c tc pc (RBnop :: RBexit None (RBtailcall sig ident args) :: nil)
   | match_block_builtin ident args dst pc' :
     c ! pc = Some (RTL.Ibuiltin ident args dst pc') ->
     valid_succ tc pc' ->
-    match_block c tc pc (RBnop :: nil) (RBbuiltin ident args dst pc')
+    match_block c tc pc (RBnop :: RBexit None (RBbuiltin ident args dst pc') :: nil)
   | match_block_cond cond args pct pcf :
     c ! pc = Some (RTL.Icond cond args pct pcf) ->
     valid_succ tc pct ->
     valid_succ tc pcf ->
-    match_block c tc pc (RBnop :: nil) (RBcond cond args pct pcf)
+    match_block c tc pc (RBnop :: RBexit None (RBcond cond args pct pcf) :: nil)
   | match_block_jumptable r ns :
     c ! pc = Some (RTL.Ijumptable r ns) ->
     Forall (valid_succ tc) ns ->
-    match_block c tc pc (RBnop :: nil) (RBjumptable r ns)
+    match_block c tc pc (RBnop :: RBexit None (RBjumptable r ns) :: nil)
   | match_block_return r :
     c ! pc = Some (RTL.Ireturn r) ->
-    match_block c tc pc (RBnop :: nil) (RBreturn r)
+    match_block c tc pc (RBnop :: RBexit None (RBreturn r) :: nil)
   .
 
 (*|
@@ -220,7 +183,7 @@ the basic block.
 |*)
 
   Definition match_code (c: RTL.code) (tc: code) : Prop :=
-    forall pc b, tc ! pc = Some b -> match_block c tc pc b.(bb_body) b.(bb_exit).
+    forall pc b, tc ! pc = Some b -> match_block c tc pc b.
 
   Variant match_stackframe : RTL.stackframe -> stackframe -> Prop :=
     | match_stackframe_init :
@@ -232,19 +195,19 @@ the basic block.
 
   Definition sem_extrap f pc sp in_s in_s' block :=
     forall out_s block2,
-      step_instr_list tge sp in_s block out_s ->
+      BB.step tge sp in_s block out_s ->
       f.(fn_code) ! pc = Some block2 ->
-      step_instr_list tge sp in_s' block2.(bb_body) out_s.
+      BB.step tge sp in_s' block2 out_s.
 
   Lemma match_block_exists_instr :
-    forall c tc pc a b,
-      match_block c tc pc a b ->
+    forall c tc pc a,
+      match_block c tc pc a ->
       exists i, c ! pc = Some i.
   Proof. inversion 1; eexists; eauto. Qed.
 
   Lemma match_block_not_nil :
-    forall c tc pc a b,
-      match_block c tc pc a b -> a <> nil.
+    forall c tc pc a,
+      match_block c tc pc a -> a <> nil.
   Proof. inversion 1; crush. Qed.
 
 (*|
@@ -261,20 +224,19 @@ proof inside of the ``match_states`` that shows that the execution from the
 whole execution (in one big step) of the basic block.
 |*)
 
-  Variant match_states : option bb -> RTL.state -> RTLBlock.state -> Prop :=
+  Variant match_states : option BB.t -> RTL.state -> state -> Prop :=
     | match_state :
       forall stk stk' f tf sp pc rs m pc0 b rs0 m0
         (TF: transl_function f = OK tf)
         (* TODO: I can remove the following [match_code]. *)
         (CODE: match_code f.(RTL.fn_code) tf.(fn_code))
-        (BLOCK: exists b',
-            tf.(fn_code) ! pc0 = Some b'
-            /\ match_block f.(RTL.fn_code) tf.(fn_code) pc b b'.(bb_exit))
+        (BLOCK: exists b', tf.(fn_code) ! pc0 = Some b'
+                           /\ match_block f.(RTL.fn_code) tf.(fn_code) pc b)
         (STK: Forall2 match_stackframe stk stk')
         (STARSIMU: star RTL.step ge (RTL.State stk f sp pc0 rs0 m0)
                                   E0 (RTL.State stk f sp pc rs m))
-        (BB: sem_extrap tf pc0 sp (mk_instr_state rs (PMap.init false) m)
-                        (mk_instr_state rs0 (PMap.init false) m0) b),
+        (BB: sem_extrap tf pc0 sp (Iexec (mk_instr_state rs (PMap.init false) m))
+                        (Iexec (mk_instr_state rs0 (PMap.init false) m0)) b),
         match_states (Some b) (RTL.State stk f sp pc rs m)
                      (State stk' tf sp pc0 rs0 (PMap.init false) m0)
     | match_callstate :
@@ -288,7 +250,7 @@ whole execution (in one big step) of the basic block.
         match_states None (RTL.Returnstate cs v m) (Returnstate cs' v m)
   .
 
-  Definition match_prog (p: RTL.program) (tp: RTLBlock.program) :=
+  Definition match_prog (p: RTL.program) (tp: GibleSeq.program) :=
     Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp.
 
   Context (TRANSL : match_prog prog tprog).
@@ -309,9 +271,9 @@ whole execution (in one big step) of the basic block.
   Proof (Genv.find_funct_ptr_transf_partial TRANSL).
 
   Lemma sig_transl_function:
-    forall (f: RTL.fundef) (tf: RTLBlock.fundef),
+    forall (f: RTL.fundef) (tf: GibleSeq.fundef),
       transl_fundef f = OK tf ->
-      RTLBlock.funsig tf = RTL.funsig f.
+      GibleSeq.funsig tf = RTL.funsig f.
   Proof using.
     unfold transl_fundef. unfold transf_partial_fundef.
     intros. destruct_match. unfold bind in *. destruct_match; try discriminate.
@@ -320,7 +282,7 @@ whole execution (in one big step) of the basic block.
     inv H; auto.
   Qed.
 
-  Definition measure (b: option bb): nat :=
+  Definition measure (b: option BB.t): nat :=
     match b with
     | None => 0
     | Some b' => 1 + length b'
@@ -359,17 +321,37 @@ whole execution (in one big step) of the basic block.
            end.
 
   Lemma transl_match_code' :
-    forall c tc b pc i,
-      check_code' c tc pc b i = true ->
-      match_block c tc pc b i.
+    forall c tc b pc,
+      check_code c tc pc b = true ->
+      match_block c tc pc b.
   Proof.
     induction b; [crush|].
-    intros. unfold check_code' in H.
-    do 4 (destruct_match; try discriminate);
-    try (repeat (destruct_match; try discriminate; []); unfold_ands; constructor; auto using check_valid_node_correct);
-    fold check_code' in *;
-    try (destruct_match; try discriminate; unfold_ands; econstructor; eauto);
-    apply Forall_forall; intros. eapply forallb_forall in H1; eauto using check_valid_node_correct.
+    - repeat (destruct_match; try discriminate).
+    - intros.
+      unfold check_code in H.
+      do 2 (destruct_match; try discriminate); subst; fold check_code in H.
+      + repeat (destruct_match; try discriminate); try solve [econstructor; eauto].
+        unfold_ands.
+        eapply match_block_goto; eauto. eauto using check_valid_node_correct.
+      + repeat (destruct_match; try discriminate); subst; try solve [unfold_ands; econstructor; eauto].
+        unfold_ands.
+        eapply match_block_op_cf; eauto. eauto using check_valid_node_correct.
+      + repeat (destruct_match; try discriminate); subst; try solve [unfold_ands; econstructor; eauto].
+        unfold_ands.
+        eapply match_block_load_cf; eauto. eauto using check_valid_node_correct.
+      + repeat (destruct_match; try discriminate); subst; try solve [unfold_ands; econstructor; eauto].
+        unfold_ands.
+        eapply match_block_store_cf; eauto. eauto using check_valid_node_correct.
+      + repeat (destruct_match; try discriminate); subst; try solve [unfold_ands; econstructor; eauto].
+        unfold_ands. eapply match_block_call; eauto using check_valid_node_correct.
+        unfold_ands. eapply match_block_call; eauto using check_valid_node_correct.
+      + repeat (destruct_match; try discriminate); subst; try solve [unfold_ands; econstructor; eauto].
+      + repeat (destruct_match; try discriminate); subst; try solve [unfold_ands; econstructor; eauto].
+        unfold_ands. eapply match_block_cond; eauto using check_valid_node_correct.
+      + repeat (destruct_match; try discriminate); subst; try solve [unfold_ands; econstructor; eauto].
+        unfold_ands. eapply match_block_jumptable; eauto using check_valid_node_correct.
+        apply Forall_forall; intros. eapply forallb_forall in H1; eauto using check_valid_node_correct.
+      + repeat (destruct_match; try discriminate); subst; try solve [unfold_ands; econstructor; eauto].
   Qed.
 
   Lemma transl_match_code :
@@ -387,7 +369,7 @@ whole execution (in one big step) of the basic block.
 
   Lemma transl_initial_states :
     forall s1, RTL.initial_state prog s1 ->
-      exists s2, RTLBlock.initial_state tprog s2 /\ match_states None s1 s2.
+      exists s2, GibleSeq.initial_state tprog s2 /\ match_states None s1 s2.
   Proof using TRANSL.
     induction 1.
     exploit function_ptr_translated; eauto. intros [tf [A B]].
@@ -402,7 +384,7 @@ whole execution (in one big step) of the basic block.
     forall s1 s2 r b,
       match_states b s1 s2 ->
       RTL.final_state s1 r ->
-      RTLBlock.final_state s2 r.
+      GibleSeq.final_state s2 r.
   Proof using.
     inversion 2; crush. subst. inv H. inv STK. econstructor.
   Qed.
@@ -459,7 +441,7 @@ whole execution (in one big step) of the basic block.
     intros * H.
     inversion 1; subst; simplify.
     unfold match_code in *.
-    match goal with H: match_block _ _ _ _ _ |- _ => inv H end; simplify.
+    match goal with H: match_block _ _ _ _ |- _ => inv H end; simplify.
     { apply sim_star.
       do 3 econstructor. eapply star_refl. constructor.
       instantiate (1 := Some b); unfold ltof; auto.
@@ -478,11 +460,11 @@ whole execution (in one big step) of the basic block.
       do 3 econstructor. apply plus_one. econstructor.
       eassumption. eapply BB; [| eassumption ].
       econstructor; econstructor; eauto.
-      setoid_rewrite <- H1. econstructor.
+      econstructor. econstructor. econstructor.
 
       econstructor; try eassumption. eauto.
       eapply star_refl.
-      unfold sem_extrap. intros. setoid_rewrite H7 in H0.
+      unfold sem_extrap. intros. setoid_rewrite H6 in H0.
       crush.
     }
   Qed.
@@ -514,13 +496,13 @@ whole execution (in one big step) of the basic block.
       Op.eval_operation ge sp op rs ## args m = Some v ->
       transl_function f = OK tf ->
       (forall pc0 b0,
-          (fn_code tf) ! pc0 = Some b0 -> match_block (RTL.fn_code f) (fn_code tf) pc0 (bb_body b0) (bb_exit b0)) ->
+          (fn_code tf) ! pc0 = Some b0 -> match_block (RTL.fn_code f) (fn_code tf) pc0 b0) ->
       Forall2 match_stackframe s stk' ->
       star RTL.step ge (RTL.State s f sp pc1 rs1 m1) E0 (RTL.State s f sp pc rs m) ->
-      sem_extrap tf pc1 sp {| is_rs := rs; is_ps := PMap.init false; is_mem := m |}
-                 {| is_rs := rs1; is_ps := PMap.init false; is_mem := m1 |} (RBop None op args res :: b) ->
+      sem_extrap tf pc1 sp (Iexec {| is_rs := rs; is_ps := PMap.init false; is_mem := m |})
+                 (Iexec {| is_rs := rs1; is_ps := PMap.init false; is_mem := m1 |}) (RBop None op args res :: b) ->
       (fn_code tf) ! pc1 = Some x ->
-      match_block (RTL.fn_code f) (fn_code tf) pc' b (bb_exit x) ->
+      match_block (RTL.fn_code f) (fn_code tf) pc' b ->
       exists b' s2',
         star step tge (State stk' tf sp pc1 rs1 (PMap.init false) m1) E0 s2'
         /\ ltof _ measure b' (Some (RBop None op args res :: b))
@@ -546,32 +528,31 @@ whole execution (in one big step) of the basic block.
       (RTL.fn_code f) ! pc = Some (RTL.Iop op args res pc') ->
       Op.eval_operation ge sp op rs ## args m = Some v ->
       transl_function f = OK tf ->
-      (forall (pc0 : positive) (b : RTLBlockInstr.bblock),
-          (fn_code tf) ! pc0 = Some b -> match_block (RTL.fn_code f) (fn_code tf) pc0 (bb_body b) (bb_exit b)) ->
+      (forall (pc0 : positive) (b : BB.t),
+          (fn_code tf) ! pc0 = Some b -> match_block (RTL.fn_code f) (fn_code tf) pc0 b) ->
       Forall2 match_stackframe s stk' ->
       star RTL.step ge (RTL.State s f sp pc1 rs1 m1) E0 (RTL.State s f sp pc rs m) ->
-      sem_extrap tf pc1 sp {| is_rs := rs; is_ps := PMap.init false; is_mem := m |}
-                 {| is_rs := rs1; is_ps := PMap.init false; is_mem := m1 |} (RBop None op args res :: nil) ->
+      sem_extrap tf pc1 sp (Iexec {| is_rs := rs; is_ps := PMap.init false; is_mem := m |})
+                 (Iexec {| is_rs := rs1; is_ps := PMap.init false; is_mem := m1 |}) (RBop None op args res :: RBexit None (RBgoto pc') :: nil) ->
       (fn_code tf) ! pc1 = Some x ->
-      RBgoto pc' = bb_exit x ->
       valid_succ (fn_code tf) pc' ->
       exists b' s2,
         plus step tge (State stk' tf sp pc1 rs1 (PMap.init false) m1) E0 s2 /\
           match_states b' (RTL.State s f sp pc' rs # res <- v m) s2.
   Proof.
-    intros * H H0 TF CODE STK STARSIMU BB H3 H2 H7.
+    intros * H H0 TF CODE STK STARSIMU BB H3 H7.
     inv H0. simplify.
     unfold valid_succ in H7; simplify.
     do 3 econstructor. apply plus_one. econstructor.
     eassumption. eapply BB; [| eassumption ].
     econstructor; econstructor; eauto.
     rewrite <- eval_op_eq; eassumption.
-    constructor. setoid_rewrite <- H2.
+    constructor. econstructor. econstructor.
     econstructor.
 
     econstructor; try eassumption. eauto.
     eapply star_refl.
-    unfold sem_extrap. intros. setoid_rewrite H0 in H5.
+    unfold sem_extrap. intros. setoid_rewrite H0 in H4.
     crush.
   Qed.
 
@@ -588,7 +569,7 @@ whole execution (in one big step) of the basic block.
     intros * H H0.
     inversion 1; subst; simplify.
     unfold match_code in *.
-    match goal with H: match_block _ _ _ _ _ |- _ => inv H end; simplify.
+    match goal with H: match_block _ _ _ _ |- _ => inv H end; simplify.
     { apply sim_star; eapply transl_Iop_correct_nj; eassumption. }
     { apply sim_plus. eapply transl_Iop_correct_j; eassumption. }
   Qed.
@@ -607,7 +588,7 @@ whole execution (in one big step) of the basic block.
     intros * H H0 H1.
     inversion 1; subst; simplify.
     unfold match_code in *.
-    match goal with H: match_block _ _ _ _ _ |- _ => inv H end; simplify.
+    match goal with H: match_block _ _ _ _ |- _ => inv H end; simplify.
     { apply sim_star.
       do 3 econstructor. eapply star_refl. constructor.
       instantiate (1 := Some b); unfold ltof; auto.
@@ -624,17 +605,17 @@ whole execution (in one big step) of the basic block.
     }
     { apply sim_plus.
       inv H0. simplify.
-      unfold valid_succ in H8; simplify.
+      unfold valid_succ in H6; simplify.
       do 3 econstructor. apply plus_one. econstructor.
       eassumption. eapply BB; [| eassumption ].
       econstructor; econstructor; eauto.
       rewrite <- eval_addressing_eq; eassumption.
-      constructor. setoid_rewrite <- H3.
+      constructor. econstructor. econstructor.
       econstructor.
 
       econstructor; try eassumption. eauto.
       eapply star_refl.
-      unfold sem_extrap. intros. setoid_rewrite H0 in H8.
+      unfold sem_extrap. intros. setoid_rewrite H0 in H6.
       crush.
     }
   Qed.
@@ -653,7 +634,7 @@ whole execution (in one big step) of the basic block.
     intros * H H0 H1.
     inversion 1; subst; simplify.
     unfold match_code in *.
-    match goal with H: match_block _ _ _ _ _ |- _ => inv H end; simplify.
+    match goal with H: match_block _ _ _ _ |- _ => inv H end; simplify.
     { apply sim_star.
       do 3 econstructor. eapply star_refl. constructor.
       instantiate (1 := Some b); unfold ltof; auto.
@@ -670,17 +651,17 @@ whole execution (in one big step) of the basic block.
     }
     { apply sim_plus.
       inv H0. simplify.
-      unfold valid_succ in H8; simplify.
+      unfold valid_succ in H6; simplify.
       do 3 econstructor. apply plus_one. econstructor.
       eassumption. eapply BB; [| eassumption ].
       econstructor; econstructor; eauto.
       rewrite <- eval_addressing_eq; eassumption.
-      constructor. setoid_rewrite <- H3.
+      constructor. econstructor. econstructor.
       econstructor.
 
       econstructor; try eassumption. eauto.
       eapply star_refl.
-      unfold sem_extrap. intros. setoid_rewrite H0 in H8.
+      unfold sem_extrap. intros. setoid_rewrite H0 in H6.
       crush.
     }
   Qed.
@@ -730,15 +711,15 @@ whole execution (in one big step) of the basic block.
     intros * H H0 H1.
     inversion 1; subst; simplify.
     unfold match_code in *.
-    match goal with H: match_block _ _ _ _ _ |- _ => inv H end; simplify;
+    match goal with H: match_block _ _ _ _ |- _ => inv H end; simplify;
     apply sim_plus.
     inv H0. simplify.
-    unfold valid_succ in H7; simplify.
+    unfold valid_succ in H5; simplify.
     exploit find_function_translated; eauto; simplify.
     do 3 econstructor. apply plus_one. econstructor.
     eassumption. eapply BB; [| eassumption ].
     econstructor; econstructor; eauto.
-    setoid_rewrite <- H1.
+    econstructor. econstructor.
     econstructor; eauto.
     apply sig_transl_function; auto.
 
@@ -756,21 +737,21 @@ whole execution (in one big step) of the basic block.
       forall b s2,
         match_states b (RTL.State s f (Vptr stk Integers.Ptrofs.zero) pc rs m) s2 ->
         exists b' s2',
-          (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option bb) measure b' b) /\
+          (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option BB.t) measure b' b) /\
             match_states b' (RTL.Callstate s fd rs ## args m') s2'.
   Proof.
     intros * H H0 H1 H2.
     inversion 1; subst; simplify.
     unfold match_code in *.
-    match goal with H: match_block _ _ _ _ _ |- _ => inv H end; simplify;
+    match goal with H: match_block _ _ _ _ |- _ => inv H end; simplify;
     apply sim_plus.
     inv H0. simplify.
-    unfold valid_succ in H7; simplify.
+    unfold valid_succ in H6; simplify.
     exploit find_function_translated; eauto; simplify.
     do 3 econstructor. apply plus_one. econstructor.
     eassumption. eapply BB; [| eassumption ].
     econstructor; econstructor; eauto.
-    setoid_rewrite <- H1.
+    econstructor. econstructor.
     econstructor; eauto.
     apply sig_transl_function; auto.
     assert (fn_stacksize tf = RTL.fn_stacksize f).
@@ -796,19 +777,19 @@ whole execution (in one big step) of the basic block.
     intros * H H0 H1.
     inversion 1; subst; simplify.
     unfold match_code in *.
-    match goal with H: match_block _ _ _ _ _ |- _ => inv H end; simplify.
+    match goal with H: match_block _ _ _ _ |- _ => inv H end; simplify.
     eapply sim_plus.
-    unfold valid_succ in H8; simplify.
+    unfold valid_succ in H6; simplify.
     do 3 econstructor. apply plus_one. econstructor.
     eassumption. eapply BB; [| eassumption ].
     econstructor; econstructor; eauto.
-    setoid_rewrite <- H3. econstructor; eauto.
+    econstructor. econstructor. econstructor; eauto.
     eauto using eval_builtin_args_preserved, symbols_preserved.
     eauto using external_call_symbols_preserved, senv_preserved.
 
     econstructor; try eassumption. eauto.
     eapply star_refl.
-    unfold sem_extrap. intros. setoid_rewrite H5 in H8. crush.
+    unfold sem_extrap. intros. setoid_rewrite H5 in H7. crush.
   Qed.
 
   Lemma init_regs_equiv :
@@ -821,7 +802,7 @@ whole execution (in one big step) of the basic block.
       forall b s2,
         match_states b (RTL.Callstate s (Internal f) args m) s2 ->
         exists b' s2',
-          (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option bb) measure b' b) /\
+          (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option BB.t) measure b' b) /\
             match_states b'
                          (RTL.State s f (Vptr stk Integers.Ptrofs.zero) (RTL.fn_entrypoint f) (RTL.init_regs args (RTL.fn_params f)) m') s2'.
   Proof.
@@ -831,7 +812,6 @@ whole execution (in one big step) of the basic block.
     pose proof (transl_match_code _ _ EQ).
     pose proof (transl_entrypoint_exists _ _ EQ). unfold valid_succ in H1.
     simplify.
-    destruct x0.
     apply sim_plus. do 3 econstructor.
     assert (fn_stacksize x = RTL.fn_stacksize f).
     { unfold transl_function in EQ.
@@ -865,7 +845,7 @@ whole execution (in one big step) of the basic block.
       forall b s2,
         match_states b (RTL.Callstate s (External ef) args m) s2 ->
         exists b' s2',
-          (plus step tge s2 t s2' \/ star step tge s2 t s2' /\ ltof (option bb) measure b' b) /\
+          (plus step tge s2 t s2' \/ star step tge s2 t s2' /\ ltof (option BB.t) measure b' b) /\
             match_states b' (RTL.Returnstate s res m') s2'.
   Proof.
     intros * H.
@@ -881,7 +861,7 @@ whole execution (in one big step) of the basic block.
     forall res f sp pc rs s vres m b s2,
       match_states b (RTL.Returnstate (RTL.Stackframe res f sp pc rs :: s) vres m) s2 ->
       exists b' s2',
-        (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option bb) measure b' b) /\
+        (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option BB.t) measure b' b) /\
           match_states b' (RTL.State s f sp pc rs # res <- vres m) s2'.
   Proof.
     intros.
@@ -904,30 +884,31 @@ whole execution (in one big step) of the basic block.
       forall b0 s2,
         match_states b0 (RTL.State s f sp pc rs m) s2 ->
         exists b' s2',
-          (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option bb) measure b' b0) /\
+          (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option BB.t) measure b' b0) /\
             match_states b' (RTL.State s f sp pc' rs m) s2'.
   Proof.
     intros * H H0 H1.
     inversion 1; subst; simplify.
     unfold match_code in *.
-    match goal with H: match_block _ _ _ _ _ |- _ => inv H end; simplify;
+    match goal with H: match_block _ _ _ _ |- _ => inv H end; simplify;
     apply sim_plus.
     inv H0. simplify.
     unfold valid_succ in *; simplify.
     destruct b.
     { do 3 econstructor. apply plus_one.
-      econstructor; eauto. eapply BB.
-      econstructor; constructor. auto.
-      setoid_rewrite <- H1. econstructor; eauto.
+      econstructor; eauto. eapply BB. econstructor. econstructor.
+      econstructor. econstructor. econstructor. eauto.
+      econstructor; eauto.
       constructor; eauto using star_refl.
-      unfold sem_extrap; intros. setoid_rewrite H4 in H8. inv H8. auto.
+      unfold sem_extrap; intros. setoid_rewrite H4 in H6. inv H6. auto.
     }
     { do 3 econstructor. apply plus_one.
       econstructor; eauto. eapply BB.
-      econstructor; constructor. auto.
-      setoid_rewrite <- H1. econstructor; eauto.
+      econstructor. econstructor.
+      econstructor. econstructor. econstructor. eauto.
+      econstructor; eauto.
       constructor; eauto using star_refl.
-      unfold sem_extrap; intros. setoid_rewrite H0 in H8. inv H8. auto.
+      unfold sem_extrap; intros. setoid_rewrite H0 in H6. inv H6. auto.
     }
   Qed.
 
@@ -939,23 +920,24 @@ whole execution (in one big step) of the basic block.
       forall b s2,
         match_states b (RTL.State s f sp pc rs m) s2 ->
         exists b' s2',
-          (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option bb) measure b' b) /\
+          (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option BB.t) measure b' b) /\
             match_states b' (RTL.State s f sp pc' rs m) s2'.
   Proof.
     intros * H H0 H1.
     inversion 1; subst; simplify.
     unfold match_code in *.
-    match goal with H: match_block _ _ _ _ _ |- _ => inv H end; simplify;
+    match goal with H: match_block _ _ _ _ |- _ => inv H end; simplify;
     apply sim_plus.
-    eapply Forall_forall with (x:=pc') in H8; eauto using list_nth_z_in.
-    unfold valid_succ in H8; simplify.
+    eapply Forall_forall with (x:=pc') in H6; eauto using list_nth_z_in.
+    unfold valid_succ in H6; simplify.
     do 3 econstructor. apply plus_one.
     econstructor; eauto. eapply BB.
-    econstructor; constructor. auto.
-    setoid_rewrite <- H3. econstructor; eauto.
+    econstructor. econstructor. econstructor. econstructor. econstructor.
+    eauto.
+    econstructor; eauto.
 
     constructor; eauto using star_refl.
-    unfold sem_extrap; intros. setoid_rewrite H5 in H8. inv H8. auto.
+    unfold sem_extrap; intros. setoid_rewrite H5 in H7. inv H7. auto.
   Qed.
 
   Lemma transl_Ireturn_correct:
@@ -965,13 +947,13 @@ whole execution (in one big step) of the basic block.
       forall b s2,
         match_states b (RTL.State s f (Vptr stk Integers.Ptrofs.zero) pc rs m) s2 ->
         exists b' s2',
-          (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option bb) measure b' b) /\
+          (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option BB.t) measure b' b) /\
             match_states b' (RTL.Returnstate s (regmap_optget or Vundef rs) m') s2'.
   Proof.
     intros * H H0.
     inversion 1; subst; simplify.
     unfold match_code in *.
-    match goal with H: match_block _ _ _ _ _ |- _ => inv H end; simplify;
+    match goal with H: match_block _ _ _ _ |- _ => inv H end; simplify;
     apply sim_plus.
     assert (fn_stacksize tf = RTL.fn_stacksize f).
     { unfold transl_function in TF.
@@ -979,9 +961,10 @@ whole execution (in one big step) of the basic block.
       inv TF; auto. }
     do 3 econstructor. apply plus_one. econstructor; eauto.
     eapply BB.
-    econstructor; constructor. auto.
-    setoid_rewrite <- H2. constructor.
-    rewrite H4. eauto.
+    econstructor. econstructor. econstructor. econstructor.
+    econstructor. eauto.
+    econstructor; eauto.
+        rewrite H4. eauto.
     constructor; eauto.
   Qed.
 
@@ -1011,11 +994,11 @@ whole execution (in one big step) of the basic block.
   Qed.
 
   Theorem transf_program_correct:
-    forward_simulation (RTL.semantics prog) (RTLBlock.semantics tprog).
+    forward_simulation (RTL.semantics prog) (GibleSeq.semantics tprog).
   Proof using TRANSL.
     eapply (Forward_simulation
               (L1:=RTL.semantics prog)
-              (L2:=RTLBlock.semantics tprog)
+              (L2:=GibleSeq.semantics tprog)
               (ltof _ measure) match_states).
     constructor.
     - apply well_founded_ltof.
diff --git a/src/hls/RTLBlockgen.v b/src/hls/RTLBlockgen.v
deleted file mode 100644
index 8f81e21..0000000
--- a/src/hls/RTLBlockgen.v
+++ /dev/null
@@ -1,299 +0,0 @@
-(*|
-..
-   Vericert: Verified high-level synthesis.
-   Copyright (C) 2020-2022 Yann Herklotz <yann@yannherklotz.com>
-
-   This program is free software: you can redistribute it and/or modify
-   it under the terms of the GNU General Public License as published by
-   the Free Software Foundation, either version 3 of the License, or
-   (at your option) any later version.
-
-   This program is distributed in the hope that it will be useful,
-   but WITHOUT ANY WARRANTY; without even the implied warranty of
-   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-   GNU General Public License for more details.
-
-   You should have received a copy of the GNU General Public License
-   along with this program.  If not, see <https://www.gnu.org/licenses/>.
-
-===========
-RTLBlockgen
-===========
-
-.. coq:: none
-|*)
-
-Require compcert.backend.RTL.
-Require Import compcert.common.AST.
-Require Import compcert.lib.Maps.
-Require Import compcert.lib.Integers.
-Require Import compcert.lib.Floats.
-
-Require Import vericert.common.DecEq.
-Require Import vericert.common.Vericertlib.
-Require Import vericert.hls.Gible.
-Require Import vericert.hls.GibleSeq.
-
-#[local] Open Scope positive.
-
-(*|
-``find_block max nodes index``: Does not need to be sorted, because we use
-filter and the max fold function to find the desired element.
-
-    Compute find_block 100 (2::94::48::39::19::nil) 40
-      = 48
-      : positive
-
-It wants to find the nearest block that is greater than or equal to the current
-block.
-|*)
-
-Definition find_block (max: positive) (nodes: list positive) (index: positive)
-  : positive :=
-  List.fold_right Pos.min max (List.filter (fun x => (index <=? x)) nodes).
-
-(*Compute (find_block 100 (2::94::48::39::19::nil) 40 =? 48).*)
-
-(*|
-.. index::
-   triple: abstract interpretation; check instruction; RTLBlockgen
-
-Check Instruction
-=================
-
-Check if an instruction is a standard instruction that should be in a basic
-block.
-|*)
-
-Definition check_instr (n: positive) (istr: RTL.instruction) (istr': instr) :=
-  match istr, istr' with
-  | RTL.Inop n', RBnop => (n' + 1 =? n)
-  | RTL.Iop op args dst n', RBop None op' args' dst' =>
-      ceq operation_eq op op' &&
-      ceq list_pos_eq args args' &&
-      ceq peq dst dst' && (n' + 1 =? n)
-  | RTL.Iload chunk addr args dst n', RBload None chunk' addr' args' dst' =>
-      ceq memory_chunk_eq chunk chunk' &&
-      ceq addressing_eq addr addr' &&
-      ceq list_pos_eq args args' &&
-      ceq peq dst dst' &&
-      (n' + 1 =? n)
-  | RTL.Istore chunk addr args src n', RBstore None chunk' addr' args' src' =>
-      ceq memory_chunk_eq chunk chunk' &&
-      ceq addressing_eq addr addr' &&
-      ceq list_pos_eq args args' &&
-      ceq peq src src' &&
-      (n' + 1 =? n)
-  | _, _ => false
-  end.
-
-Definition check_cf_instr_body (istr: RTL.instruction) (istr': instr): bool :=
-  match istr, istr' with
-  | RTL.Iop op args dst _, RBop None op' args' dst' =>
-      ceq operation_eq op op' &&
-      ceq list_pos_eq args args' &&
-      ceq peq dst dst'
-  | RTL.Iload chunk addr args dst _, RBload None chunk' addr' args' dst' =>
-      ceq memory_chunk_eq chunk chunk' &&
-      ceq addressing_eq addr addr' &&
-      ceq list_pos_eq args args' &&
-      ceq peq dst dst'
-  | RTL.Istore chunk addr args src _, RBstore None chunk' addr' args' src' =>
-      ceq memory_chunk_eq chunk chunk' &&
-      ceq addressing_eq addr addr' &&
-      ceq list_pos_eq args args' &&
-      ceq peq src src'
-  | RTL.Inop _, RBnop
-  | RTL.Icall _ _ _ _ _, RBnop
-  | RTL.Itailcall _ _ _, RBnop
-  | RTL.Ibuiltin _ _ _ _, RBnop
-  | RTL.Icond _ _ _ _, RBnop
-  | RTL.Ijumptable _ _, RBnop
-  | RTL.Ireturn _, RBnop => true
-  | _, _ => false
-  end.
-
-Definition check_cf_instr (istr: RTL.instruction) (istr': cf_instr) :=
-  match istr, istr' with
-  | RTL.Inop n, RBgoto n' => (n =? n')
-  | RTL.Iop _ _ _ n, RBgoto n' => (n =? n')
-  | RTL.Iload _ _ _ _ n, RBgoto n' => (n =? n')
-  | RTL.Istore _ _ _ _ n, RBgoto n' => (n =? n')
-  | RTL.Icall sig (inl r) args dst n, RBcall sig' (inl r') args' dst' n' =>
-      ceq signature_eq sig sig' &&
-      ceq peq r r' &&
-      ceq list_pos_eq args args' &&
-      ceq peq dst dst' &&
-      (n =? n')
-  | RTL.Icall sig (inr i) args dst n, RBcall sig' (inr i') args' dst' n' =>
-      ceq signature_eq sig sig' &&
-      ceq peq i i' &&
-      ceq list_pos_eq args args' &&
-      ceq peq dst dst' &&
-      (n =? n')
-  | RTL.Itailcall sig (inl r) args, RBtailcall sig' (inl r') args' =>
-      ceq signature_eq sig sig' &&
-      ceq peq r r' &&
-      ceq list_pos_eq args args'
-  | RTL.Itailcall sig (inr r) args, RBtailcall sig' (inr r') args' =>
-      ceq signature_eq sig sig' &&
-      ceq peq r r' &&
-      ceq list_pos_eq args args'
-  | RTL.Icond cond args n1 n2, RBcond cond' args' n1' n2' =>
-      ceq condition_eq cond cond' &&
-      ceq list_pos_eq args args' &&
-      ceq peq n1 n1' && ceq peq n2 n2'
-  | RTL.Ijumptable r ns, RBjumptable r' ns' =>
-      ceq peq r r' && ceq list_pos_eq ns ns'
-  | RTL.Ireturn (Some r), RBreturn (Some r') =>
-      ceq peq r r'
-  | RTL.Ireturn None, RBreturn None => true
-  | _, _ => false
-  end.
-
-Definition is_cf_instr (n: positive) (i: RTL.instruction) :=
-  match i with
-  | RTL.Inop n' => negb (n' + 1 =? n)
-  | RTL.Iop _ _ _ n' => negb (n' + 1 =? n)
-  | RTL.Iload _ _ _ _ n' => negb (n' + 1 =? n)
-  | RTL.Istore _ _ _ _ n' => negb (n' + 1 =? n)
-  | RTL.Icall _ _ _ _ _ => true
-  | RTL.Itailcall _ _ _ => true
-  | RTL.Ibuiltin _ _ _ _ => true
-  | RTL.Icond _ _ _ _ => true
-  | RTL.Ijumptable _ _ => true
-  | RTL.Ireturn _ => true
-  end.
-
-Definition check_present_blocks (c: code) (n: list positive) (max: positive) (i: positive) (istr: RTL.instruction) :=
-  let blockn := find_block max n i in
-  match c ! blockn with
-  | Some istrs =>
-      match List.nth_error istrs.(bb_body) (Pos.to_nat blockn - Pos.to_nat i)%nat with
-      | Some istr' =>
-          if is_cf_instr i istr
-          then check_cf_instr istr istrs.(bb_exit) && check_cf_instr_body istr istr'
-          else check_instr i istr istr'
-      | None => false
-      end
-  | None => false
-  end.
-
-Definition check_valid_node (tc: code) (e: node) :=
-  match tc ! e with
-  | Some _ => true
-  | _ => false
-  end.
-
-Fixpoint check_code' (c: RTL.code) (tc: code) (pc: node) (b: bb) (i: cf_instr) :=
-  match b, i, c ! pc with
-  | RBnop :: (_ :: _) as b', _, Some (RTL.Inop pc') =>
-      check_code' c tc pc' b' i
-  | RBop None op args dst :: (_ :: _) as b', _, Some (RTL.Iop op' args' dst' pc') =>
-      ceq operation_eq op op'
-      && ceq list_pos_eq args args'
-      && ceq peq dst dst'
-      && check_code' c tc pc' b' i
-  | RBload None chunk addr args dst :: (_ :: _) as b', _,
-    Some (RTL.Iload chunk' addr' args' dst' pc') =>
-      ceq memory_chunk_eq chunk chunk'
-      && ceq addressing_eq addr addr'
-      && ceq list_pos_eq args args'
-      && ceq peq dst dst'
-      && check_code' c tc pc' b' i
-  | RBstore None chunk addr args src :: (_ :: _) as b', _,
-    Some (RTL.Istore chunk' addr' args' src' pc') =>
-      ceq memory_chunk_eq chunk chunk'
-      && ceq addressing_eq addr addr'
-      && ceq list_pos_eq args args'
-      && ceq peq src src'
-      && check_code' c tc pc' b' i
-  | RBnop :: nil, RBgoto pc', Some (RTL.Inop pc'') =>
-      check_valid_node tc pc'
-      && ceq peq pc' pc''
-  | RBop None op args dst :: nil, RBgoto pc', Some (RTL.Iop op' args' dst' pc'') =>
-      check_valid_node tc pc'
-      && ceq peq pc' pc''
-      && ceq operation_eq op op'
-      && ceq list_pos_eq args args'
-      && ceq peq dst dst'
-  | RBload None chunk addr args dst :: nil, RBgoto pc',
-    Some (RTL.Iload chunk' addr' args' dst' pc'') =>
-      check_valid_node tc pc'
-      && ceq peq pc' pc''
-      && ceq memory_chunk_eq chunk chunk'
-      && ceq addressing_eq addr addr'
-      && ceq list_pos_eq args args'
-      && ceq peq dst dst'
-  | RBstore None chunk addr args src :: nil, RBgoto pc',
-    Some (RTL.Istore chunk' addr' args' src' pc'') =>
-      check_valid_node tc pc'
-      && ceq peq pc' pc''
-      && ceq memory_chunk_eq chunk chunk'
-      && ceq addressing_eq addr addr'
-      && ceq list_pos_eq args args'
-      && ceq peq src src'
-  | RBnop :: nil, RBcall sig (inl r) args dst pc',
-    Some (RTL.Icall sig' (inl r') args' dst' pc'') =>
-      check_valid_node tc pc'
-      && ceq peq pc' pc''
-      && ceq signature_eq sig sig'
-      && ceq peq r r'
-      && ceq list_pos_eq args args'
-      && ceq peq dst dst'
-  | RBnop :: nil, RBcall sig (inr i) args dst pc',
-    Some (RTL.Icall sig' (inr i') args' dst' pc'') =>
-      check_valid_node tc pc'
-      && ceq peq pc' pc''
-      && ceq signature_eq sig sig'
-      && ceq peq i i'
-      && ceq list_pos_eq args args'
-      && ceq peq dst dst'
-  | RBnop :: nil, RBtailcall sig' (inl r') args',
-    Some (RTL.Itailcall sig (inl r) args) =>
-      ceq signature_eq sig sig'
-      && ceq peq r r'
-      && ceq list_pos_eq args args'
-  | RBnop :: nil, RBtailcall sig' (inr r') args',
-    Some (RTL.Itailcall sig (inr r) args) =>
-      ceq signature_eq sig sig'
-      && ceq peq r r'
-      && ceq list_pos_eq args args'
-  | RBnop :: nil, RBcond cond' args' n1' n2', Some (RTL.Icond cond args n1 n2) =>
-      check_valid_node tc n1
-      && check_valid_node tc n2
-      && ceq condition_eq cond cond'
-      && ceq list_pos_eq args args'
-      && ceq peq n1 n1'
-      && ceq peq n2 n2'
-  | RBnop :: nil, RBjumptable r' ns', Some (RTL.Ijumptable r ns) =>
-      ceq peq r r'
-      && ceq list_pos_eq ns ns'
-      && forallb (check_valid_node tc) ns
-  | RBnop :: nil, RBreturn (Some r'), Some (RTL.Ireturn (Some r)) =>
-      ceq peq r r'
-  | RBnop :: nil, RBreturn None, Some (RTL.Ireturn None) => true
-  | _, _, _ => false
-  end.
-
-Definition check_code c tc pc b :=
-  check_code' c tc pc b.(bb_body) b.(bb_exit).
-
-Parameter partition : RTL.function -> Errors.res function.
-
-Definition transl_function (f: RTL.function) :=
-  match partition f with
-  | Errors.OK f' =>
-      if check_valid_node f'.(fn_code) f.(RTL.fn_entrypoint) then
-        if forall_ptree (check_code f.(RTL.fn_code) f'.(fn_code)) f'.(fn_code) then
-          Errors.OK
-            (mkfunction f.(RTL.fn_sig) f.(RTL.fn_params) f.(RTL.fn_stacksize) f'.(fn_code) f.(RTL.fn_entrypoint))
-        else Errors.Error (Errors.msg "check_present_blocks failed")
-      else Errors.Error (Errors.msg "entrypoint does not exists")
-  | Errors.Error msg => Errors.Error msg
-  end.
-
-Definition transl_fundef := transf_partial_fundef transl_function.
-
-Definition transl_program : RTL.program -> Errors.res program :=
-  transform_partial_program transl_fundef.