Translate the base languages

7 files changed, 431 insertions, 437 deletions

diff --git a/src/hls/RTLBlockInstr.v b/src/hls/Gible.v
index 2d48650..22d25f8 100644
--- a/src/hls/RTLBlockInstr.v
+++ b/src/hls/Gible.v
@@ -35,6 +35,7 @@ Require Import compcert.common.Globalenvs.
 Require Import compcert.common.Memory.
 Require Import compcert.common.Values.
 Require Import compcert.lib.Integers.
+Require Import compcert.common.Smallstep.
 Require Import compcert.lib.Maps.
 Require Import compcert.verilog.Op.
 
@@ -56,17 +57,6 @@ is that these instructions don't have a next node, as they will be in a basic
 block, and they also have an optional predicate (``pred_op``).
 |*)
 
-Inductive instr : Type :=
-| RBnop : instr
-| RBop :
-  option pred_op -> operation -> list reg -> reg -> instr
-| RBload :
-  option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr
-| RBstore :
-  option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr
-| RBsetpred :
-  option pred_op -> condition -> list reg -> predicate -> instr.
-
 (*|
 .. index::
    triple: definition; RTLBlockInstr; control-flow instruction
@@ -89,6 +79,18 @@ Inductive cf_instr : Type :=
 | RBgoto : node -> cf_instr
 | RBpred_cf : pred_op -> cf_instr -> cf_instr -> cf_instr.
 
+Inductive instr : Type :=
+| RBnop : instr
+| RBop :
+  option pred_op -> operation -> list reg -> reg -> instr
+| RBload :
+  option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr
+| RBstore :
+  option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr
+| RBsetpred :
+  option pred_op -> condition -> list reg -> predicate -> instr
+| RBexit : option pred_op -> cf_instr -> instr.
+
 (*|
 Helper Functions
 ================
@@ -107,19 +109,6 @@ Fixpoint successors_instr (i : cf_instr) : list node :=
       concat (successors_instr c1 :: successors_instr c2 :: nil)
   end.
 
-Definition max_reg_instr (m: positive) (i: instr) :=
-  match i with
-  | RBnop => m
-  | RBop p op args res =>
-      fold_left Pos.max args (Pos.max res m)
-  | RBload p chunk addr args dst =>
-      fold_left Pos.max args (Pos.max dst m)
-  | RBstore p chunk addr args src =>
-      fold_left Pos.max args (Pos.max src m)
-  | RBsetpred p' c args p =>
-      fold_left Pos.max args m
-  end.
-
 Fixpoint max_reg_cfi (m : positive) (i : cf_instr) :=
   match i with
   | RBcall sig (inl r) args res s =>
@@ -141,6 +130,20 @@ Fixpoint max_reg_cfi (m : positive) (i : cf_instr) :=
   | RBpred_cf p c1 c2 => Pos.max (max_reg_cfi m c1) (max_reg_cfi m c2)
   end.
 
+Definition max_reg_instr (m: positive) (i: instr) :=
+  match i with
+  | RBnop => m
+  | RBop p op args res =>
+      fold_left Pos.max args (Pos.max res m)
+  | RBload p chunk addr args dst =>
+      fold_left Pos.max args (Pos.max dst m)
+  | RBstore p chunk addr args src =>
+      fold_left Pos.max args (Pos.max src m)
+  | RBsetpred p' c args p =>
+      fold_left Pos.max args m
+  | RBexit _ c => max_reg_cfi m c
+  end.
+
 Definition regset := Regmap.t val.
 Definition predset := PMap.t bool.
 
@@ -203,21 +206,119 @@ Record instr_state := mk_instr_state {
                          is_mem: mem;
                        }.
 
+Variant istate : Type :=
+  | Iexec : instr_state -> istate
+  | Iterm : instr_state -> cf_instr -> istate.
+
+Inductive eval_pred:
+  option pred_op -> instr_state -> instr_state -> instr_state -> Prop :=
+| eval_pred_true:
+  forall i i' p,
+    eval_predf (is_ps i) p = true ->
+    eval_pred (Some p) i i' i'
+| eval_pred_false:
+  forall i i' p,
+    eval_predf (is_ps i) p = false ->
+    eval_pred (Some p) i i' i
+| eval_pred_none:
+  forall i i', eval_pred None i i' i'.
+
+Section RELABSTR.
+
+  Context {A B : Type} (ge : Genv.t A B).
+
+(*|
+.. index::
+   triple: semantics; RTLBlockInstr; instruction
+
+Step Instruction
+=============================
+|*)
+
+Variant step_instr: val -> istate -> instr -> istate -> Prop :=
+  | exec_RBnop:
+    forall sp ist,
+      step_instr sp ist RBnop ist
+  | exec_RBop:
+    forall op v res args rs m sp p ist 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)
+  | exec_RBload:
+    forall addr rs args a chunk m v dst sp p pr ist,
+      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 ->
+      step_instr sp (Iexec (mk_instr_state rs pr m))
+                 (RBload p chunk addr args dst) (Iexec ist)
+  | exec_RBstore:
+    forall addr rs args a chunk m src m' sp p pr ist,
+      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 ->
+      step_instr sp (Iexec (mk_instr_state rs pr m))
+                 (RBstore p chunk addr args src) (Iexec ist)
+  | exec_RBsetpred:
+    forall sp rs pr m p c b args p' ist,
+      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 ->
+      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)
+.
+
+End RELABSTR.
+
+(*|
+A big-step semantics describing the execution of a list of instructions.  This
+uses a higher-order function ``step_i``, so that this ``Inductive`` can be
+nested to describe the execution of nested lists.
+|*)
+
+Inductive step_list {A} (step_i: val -> istate -> A -> istate -> Prop):
+  val -> istate -> list A -> istate -> Prop :=
+| exec_RBcons:
+  forall state i state' state'' instrs sp,
+    step_i sp state i state' ->
+    step_list step_i sp state' instrs state'' ->
+    step_list step_i sp state (i :: instrs) state''
+| exec_RBnil:
+  forall state sp,
+    step_list step_i sp state nil state.
+
 (*|
 Top-Level Type Definitions
 ==========================
 |*)
 
-Section DEFINITION.
+Module Type BlockType.
+
+  Parameter t: Type.
+
+  Section STEP.
+    Context {A B : Type}.
+    Parameter step: Genv.t A B -> val -> istate -> t -> istate -> Prop.
+  End STEP.
 
-  Context {bblock_body: Type}.
+  Parameter max_reg : positive -> node -> t -> positive.
 
-  Record bblock : Type := mk_bblock {
-                             bb_body: bblock_body;
-                             bb_exit: cf_instr
-                           }.
+  Parameter length : t -> nat.
 
-  Definition code: Type := PTree.t bblock.
+End BlockType.
+
+Module Gible(B : BlockType).
+
+  Definition code: Type := PTree.t B.t.
 
   Record function: Type := mkfunction {
                               fn_sig: signature;
@@ -279,8 +380,6 @@ though is that executing basic blocks uses big-step semantics.
              (m: mem),                (**r memory state *)
         state.
 
-End DEFINITION.
-
 (*|
 Old version of state
 ~~~~~~~~~~~~~~~~~~~~
@@ -324,167 +423,173 @@ Semantics
 =========
 |*)
 
-Section RELSEM.
+  Section RELSEM.
 
-  Context {bblock_body : Type}.
+    Definition genv := Genv.t fundef unit.
 
-  Definition genv := Genv.t (@fundef bblock_body) unit.
+    Context (ge: genv).
 
-  Context (ge: genv).
-
-  Definition find_function
-             (ros: reg + ident) (rs: regset) : option fundef :=
-    match ros with
-    | inl r => Genv.find_funct ge rs#r
-    | inr symb =>
-        match Genv.find_symbol ge symb with
-        | None => None
-        | Some b => Genv.find_funct_ptr ge b
-        end
-    end.
-
-  Inductive eval_pred:
-    option pred_op -> instr_state -> instr_state -> instr_state -> Prop :=
-  | eval_pred_true:
-    forall i i' p,
-      eval_predf (is_ps i) p = true ->
-      eval_pred (Some p) i i' i'
-  | eval_pred_false:
-    forall i i' p,
-      eval_predf (is_ps i) p = false ->
-      eval_pred (Some p) i i' i
-  | eval_pred_none:
-    forall i i', eval_pred None i i' i'.
+    Definition find_function
+               (ros: reg + ident) (rs: regset) : option fundef :=
+      match ros with
+      | inl r => Genv.find_funct ge rs#r
+      | inr symb =>
+          match Genv.find_symbol ge symb with
+          | None => None
+          | Some b => Genv.find_funct_ptr ge b
+          end
+      end.
 
 (*|
 .. index::
-   triple: semantics; RTLBlockInstr; instruction
+   triple: semantics; RTLBlockInstr; control-flow instruction
 
-Step Instruction
+Step Control-Flow Instruction
 =============================
+
+These control-flow instruction semantics are essentially the same as in RTL,
+with the addition of a recursive conditional instruction, which is used to
+support if-conversion.
 |*)
 
-  Variant step_instr: val -> instr_state -> instr -> instr_state -> Prop :=
-  | exec_RBnop:
-    forall sp ist,
-      step_instr sp ist RBnop ist
-  | exec_RBop:
-    forall op v res args rs m sp p ist 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 (mk_instr_state rs pr m) (RBop p op args res) ist
-  | exec_RBload:
-    forall addr rs args a chunk m v dst sp p pr ist,
-      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 ->
-      step_instr sp (mk_instr_state rs pr m)
-                 (RBload p chunk addr args dst) ist
-  | exec_RBstore:
-    forall addr rs args a chunk m src m' sp p pr ist,
-      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 ->
-      step_instr sp (mk_instr_state rs pr m)
-                 (RBstore p chunk addr args src) ist
-  | exec_RBsetpred:
-    forall sp rs pr m p c b args p' ist,
-      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 ->
-      step_instr sp (mk_instr_state rs pr m)
-                 (RBsetpred p' c args p) ist.
+    Inductive step_cf_instr: state -> cf_instr -> trace -> state -> Prop :=
+    | exec_RBcall:
+      forall s f sp rs m res fd ros sig args pc pc' pr,
+        find_function ros rs = Some fd ->
+        funsig fd = sig ->
+        step_cf_instr
+          (State s f sp pc rs pr m) (RBcall sig ros args res pc')
+          E0 (Callstate (Stackframe res f sp pc' rs pr :: s) fd rs##args m)
+    | exec_RBtailcall:
+      forall s f stk rs m sig ros args fd m' pc pr,
+        find_function ros rs = Some fd ->
+        funsig fd = sig ->
+        Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
+        step_cf_instr
+          (State s f (Vptr stk Ptrofs.zero) pc rs pr m)
+          (RBtailcall sig ros args)
+          E0 (Callstate s fd rs##args m')
+    | exec_RBbuiltin:
+      forall s f sp rs m ef args res pc' vargs t vres m' pc pr,
+        eval_builtin_args ge (fun r => rs#r) sp m args vargs ->
+        external_call ef ge vargs m t vres m' ->
+        step_cf_instr
+          (State s f sp pc rs pr m) (RBbuiltin ef args res pc')
+          t (State s f sp pc' (regmap_setres res vres rs) pr m')
+    | exec_RBcond:
+      forall s f sp rs m cond args ifso ifnot b pc pc' pr,
+        eval_condition cond rs##args m = Some b ->
+        pc' = (if b then ifso else ifnot) ->
+        step_cf_instr
+          (State s f sp pc rs pr m)
+          (RBcond cond args ifso ifnot)
+          E0 (State s f sp pc' rs pr m)
+    | exec_RBjumptable:
+      forall s f sp rs m arg tbl n pc pc' pr,
+        rs#arg = Vint n ->
+        list_nth_z tbl (Int.unsigned n) = Some pc' ->
+        step_cf_instr
+          (State s f sp pc rs pr m)
+          (RBjumptable arg tbl)
+          E0 (State s f sp pc' rs pr m)
+    | exec_RBreturn:
+      forall s f stk rs m or pc m' pr,
+        Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
+        step_cf_instr
+          (State s f (Vptr stk Ptrofs.zero) pc rs pr m)
+          (RBreturn or)
+          E0 (Returnstate s (regmap_optget or Vundef rs) m')
+    | exec_RBgoto:
+      forall s f sp pc rs pr m pc',
+        step_cf_instr (State s f sp pc rs pr m)
+                      (RBgoto pc') E0 (State s f sp pc' rs pr m)
+    | exec_RBpred_cf:
+      forall s f sp pc rs pr m cf1 cf2 st' p t,
+        step_cf_instr
+          (State s f sp pc
+                 rs pr m) (if eval_predf pr p then cf1 else cf2) t st' ->
+        step_cf_instr
+          (State s f sp pc rs pr m) (RBpred_cf p cf1 cf2)
+          t st'.
 
 (*|
-A big-step semantics describing the execution of a list of instructions.  This
-uses a higher-order function ``step_i``, so that this ``Inductive`` can be
-nested to describe the execution of nested lists.
+Top-level step
+--------------
+
+The step function itself then uses this big step of the list of instructions to
+then show a transition from basic block to basic block.  The one particular
+aspect of this is that the basic block is also part of the state, which has to
+be correctly set during the execution of the function.  Function calls and
+function returns then also need to set the basic block properly.  This means
+that the basic block of the returning function also needs to be stored in the
+stackframe, as that is the only assumption one can make when returning from a
+function.
 |*)
 
-  Inductive step_list {A} (step_i: val -> instr_state -> A -> instr_state -> Prop):
-    val -> instr_state -> list A -> instr_state -> Prop :=
-  | exec_RBcons:
-    forall state i state' state'' instrs sp,
-      step_i sp state i state' ->
-      step_list step_i sp state' instrs state'' ->
-      step_list step_i sp state (i :: instrs) state''
-  | exec_RBnil:
-    forall state sp,
-      step_list step_i sp state nil state.
+    Variant step: state -> trace -> state -> Prop :=
+      | exec_bblock:
+        forall s f sp pc rs rs' m m' bb pr pr' t state cf,
+          f.(fn_code) ! pc = Some bb ->
+          B.step ge sp (Iexec (mk_instr_state rs pr m)) bb (Iterm (mk_instr_state rs' pr' m') cf) ->
+          step_cf_instr (State s f sp pc rs' pr' m') cf t state ->
+          step (State s f sp pc rs pr m) t state
+      | exec_function_internal:
+        forall s f args m m' stk,
+          Mem.alloc m 0 f.(fn_stacksize) = (m', stk) ->
+          step (Callstate s (Internal f) args m)
+               E0 (State s f
+                         (Vptr stk Ptrofs.zero)
+                         f.(fn_entrypoint)
+                         (init_regs args f.(fn_params))
+                         (PMap.init false)
+                         m')
+      | exec_function_external:
+        forall s ef args res t m m',
+          external_call ef ge args m t res m' ->
+          step (Callstate s (External ef) args m)
+               t (Returnstate s res m')
+      | exec_return:
+        forall res f sp pc rs s vres m pr,
+          step (Returnstate (Stackframe res f sp pc rs pr :: s) vres m)
+               E0 (State s f sp pc (rs#res <- vres) pr m).
+
+  End RELSEM.
+
+  Inductive initial_state (p: program): state -> Prop :=
+  | initial_state_intro: forall b f m0,
+      let ge := Genv.globalenv p in
+      Genv.init_mem p = Some m0 ->
+      Genv.find_symbol ge p.(prog_main) = Some b ->
+      Genv.find_funct_ptr ge b = Some f ->
+      funsig f = signature_main ->
+      initial_state p (Callstate nil f nil m0).
+
+  Inductive final_state: state -> int -> Prop :=
+  | final_state_intro: forall r m,
+      final_state (Returnstate nil (Vint r) m) r.
 
 (*|
-.. index::
-   triple: semantics; RTLBlockInstr; control-flow instruction
-
-Step Control-Flow Instruction
-=============================
+Semantics
+=========
 
-These control-flow instruction semantics are essentially the same as in RTL,
-with the addition of a recursive conditional instruction, which is used to
-support if-conversion.
+We first describe the semantics by assuming a global program environment with
+type ~genv~ which was declared earlier.
 |*)
 
-  Inductive step_cf_instr: state -> cf_instr -> trace -> state -> Prop :=
-  | exec_RBcall:
-    forall s f sp rs m res fd ros sig args pc pc' pr,
-      find_function ros rs = Some fd ->
-      funsig fd = sig ->
-      step_cf_instr
-        (State s f sp pc rs pr m) (RBcall sig ros args res pc')
-        E0 (Callstate (Stackframe res f sp pc' rs pr :: s) fd rs##args m)
-  | exec_RBtailcall:
-    forall s f stk rs m sig ros args fd m' pc pr,
-      find_function ros rs = Some fd ->
-      funsig fd = sig ->
-      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
-      step_cf_instr
-        (State s f (Vptr stk Ptrofs.zero) pc rs pr m)
-        (RBtailcall sig ros args)
-        E0 (Callstate s fd rs##args m')
-  | exec_RBbuiltin:
-    forall s f sp rs m ef args res pc' vargs t vres m' pc pr,
-      eval_builtin_args ge (fun r => rs#r) sp m args vargs ->
-      external_call ef ge vargs m t vres m' ->
-      step_cf_instr
-        (State s f sp pc rs pr m) (RBbuiltin ef args res pc')
-        t (State s f sp pc' (regmap_setres res vres rs) pr m')
-  | exec_RBcond:
-    forall s f sp rs m cond args ifso ifnot b pc pc' pr,
-      eval_condition cond rs##args m = Some b ->
-      pc' = (if b then ifso else ifnot) ->
-      step_cf_instr
-        (State s f sp pc rs pr m)
-        (RBcond cond args ifso ifnot)
-        E0 (State s f sp pc' rs pr m)
-  | exec_RBjumptable:
-    forall s f sp rs m arg tbl n pc pc' pr,
-      rs#arg = Vint n ->
-      list_nth_z tbl (Int.unsigned n) = Some pc' ->
-      step_cf_instr
-        (State s f sp pc rs pr m)
-        (RBjumptable arg tbl)
-        E0 (State s f sp pc' rs pr m)
-  | exec_RBreturn:
-    forall s f stk rs m or pc m' pr,
-      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
-      step_cf_instr
-        (State s f (Vptr stk Ptrofs.zero) pc rs pr m)
-        (RBreturn or)
-        E0 (Returnstate s (regmap_optget or Vundef rs) m')
-  | exec_RBgoto:
-    forall s f sp pc rs pr m pc',
-      step_cf_instr (State s f sp pc rs pr m)
-                    (RBgoto pc') E0 (State s f sp pc' rs pr m)
-  | exec_RBpred_cf:
-    forall s f sp pc rs pr m cf1 cf2 st' p t,
-      step_cf_instr
-        (State s f sp pc
-               rs pr m) (if eval_predf pr p then cf1 else cf2) t st' ->
-      step_cf_instr
-        (State s f sp pc rs pr m) (RBpred_cf p cf1 cf2)
-        t st'.
-
-End RELSEM.
+  Definition semantics (p: program) :=
+    Semantics step (initial_state p) final_state (Genv.globalenv p).
+
+  Definition max_reg_function (f: function) :=
+    Pos.max
+      (PTree.fold B.max_reg f.(fn_code) 1%positive)
+      (fold_left Pos.max f.(fn_params) 1%positive).
+
+  Definition max_pc_function (f: function) : positive :=
+    PTree.fold
+      (fun m pc i =>
+         (Pos.max m
+                  (pc + match Z.of_nat (B.length i)
+                        with Z.pos p => p | _ => 1 end))%positive)
+      f.(fn_code) 1%positive.
+
+End Gible.
diff --git a/src/hls/GiblePar.v b/src/hls/GiblePar.v
new file mode 100644
index 0000000..8eb06ae
--- /dev/null
+++ b/src/hls/GiblePar.v
@@ -0,0 +1,75 @@
+(*
+ * 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/>.
+ *)
+
+Require Import compcert.backend.Registers.
+Require Import compcert.common.AST.
+Require Import compcert.common.Events.
+Require Import compcert.common.Globalenvs.
+Require Import compcert.common.Memory.
+Require Import compcert.common.Smallstep.
+Require Import compcert.common.Values.
+Require Import compcert.lib.Coqlib.
+Require Import compcert.lib.Integers.
+Require Import compcert.lib.Maps.
+Require Import compcert.verilog.Op.
+Require Import vericert.hls.Gible.
+
+(*|
+========
+RTLBlock
+========
+|*)
+
+Module BB <: BlockType.
+
+  Definition t := list (list (list instr)).
+
+  Section RELSEM.
+
+    Context {A B: Type} (ge: Genv.t A B).
+
+    Definition step_instr_list := step_list (step_instr ge).
+    Definition step_instr_seq := step_list step_instr_list.
+    Definition step_instr_block := step_list step_instr_seq.
+
+(*|
+Instruction list step
+---------------------
+
+The ``step_instr_list`` definition describes the execution of a list of
+instructions in one big step, inductively traversing the list of instructions
+and applying the ``step_instr``.
+
+This is simply using the high-level function ``step_list``, which is a general
+function that can execute lists of things, given their execution rule.
+|*)
+
+    Definition step := step_instr_block.
+
+  End RELSEM.
+
+  Definition max_reg (m : positive) (pc : node) (bb : t) :=
+    fold_left
+      (fun x l => fold_left (fun x' l' => fold_left max_reg_instr l' x') l x)
+      bb m.
+
+  Definition length : t -> nat := @length (list (list instr)).
+
+End BB.
+
+Module GiblePar := Gible(BB).
diff --git a/src/hls/GibleSeq.v b/src/hls/GibleSeq.v
new file mode 100644
index 0000000..321d639
--- /dev/null
+++ b/src/hls/GibleSeq.v
@@ -0,0 +1,70 @@
+(*
+ * 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/>.
+ *)
+
+Require Import compcert.backend.Registers.
+Require Import compcert.common.AST.
+Require Import compcert.common.Events.
+Require Import compcert.common.Globalenvs.
+Require Import compcert.common.Memory.
+Require Import compcert.common.Smallstep.
+Require Import compcert.common.Values.
+Require Import compcert.lib.Coqlib.
+Require Import compcert.lib.Integers.
+Require Import compcert.lib.Maps.
+Require Import compcert.verilog.Op.
+
+Require Import vericert.hls.Gible.
+
+(*|
+========
+RTLBlock
+========
+|*)
+
+Module BB <: BlockType.
+
+  Definition t := list instr.
+
+  Section RELSEM.
+
+    Context {A B: Type} (ge: Genv.t A B).
+
+(*|
+Instruction list step
+---------------------
+
+The ``step_instr_list`` definition describes the execution of a list of
+instructions in one big step, inductively traversing the list of instructions
+and applying the ``step_instr``.
+
+This is simply using the high-level function ``step_list``, which is a general
+function that can execute lists of things, given their execution rule.
+|*)
+
+    Definition step := step_list (step_instr ge).
+
+  End RELSEM.
+
+  Definition max_reg (m : positive) (n: node) (i : t) : positive :=
+    fold_left max_reg_instr i m.
+
+  Definition length : t -> nat := @length instr.
+
+End BB.
+
+Module GibleSeq := Gible(BB).
diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v
index 2516109..4e62a68 100644
--- a/src/hls/IfConversion.v
+++ b/src/hls/IfConversion.v
@@ -106,7 +106,7 @@ Fixpoint get_loops (b: bourdoncle): list node :=
   end.
 
 Definition is_loop (b: list node) (n: node) :=
-  any (fun x => Pos.eqb x n) b.
+  any (Pos.eqb n) b.
 
 Definition is_flat_cfi (n: cf_instr) :=
   match n with
diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v
deleted file mode 100644
index 19ac4f5..0000000
--- a/src/hls/RTLBlock.v
+++ /dev/null
@@ -1,137 +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/>.
- *)
-
-Require Import compcert.backend.Registers.
-Require Import compcert.common.AST.
-Require Import compcert.common.Events.
-Require Import compcert.common.Globalenvs.
-Require Import compcert.common.Memory.
-Require Import compcert.common.Smallstep.
-Require Import compcert.common.Values.
-Require Import compcert.lib.Coqlib.
-Require Import compcert.lib.Integers.
-Require Import compcert.lib.Maps.
-Require Import compcert.verilog.Op.
-
-Require Import vericert.hls.RTLBlockInstr.
-
-(*|
-========
-RTLBlock
-========
-|*)
-
-Definition bb := list instr.
-
-Definition bblock := @bblock bb.
-Definition code := @code bb.
-Definition function := @function bb.
-Definition fundef := @fundef bb.
-Definition program := @program bb.
-Definition funsig := @funsig bb.
-Definition stackframe := @stackframe bb.
-Definition state := @state bb.
-
-Definition genv := @genv bb.
-
-(*|
-Semantics
-=========
-
-We first describe the semantics by assuming a global program environment with
-type ~genv~ which was declared earlier.
-|*)
-
-Section RELSEM.
-
-  Context (ge: genv).
-
-(*|
-Instruction list step
----------------------
-
-The ``step_instr_list`` definition describes the execution of a list of
-instructions in one big step, inductively traversing the list of instructions
-and applying the ``step_instr``.
-
-This is simply using the high-level function ``step_list``, which is a general
-function that can execute lists of things, given their execution rule.
-|*)
-
-  Definition step_instr_list := step_list (step_instr ge).
-
-(*|
-Top-level step
---------------
-
-The step function itself then uses this big step of the list of instructions to
-then show a transition from basic block to basic block.  The one particular
-aspect of this is that the basic block is also part of the state, which has to
-be correctly set during the execution of the function.  Function calls and
-function returns then also need to set the basic block properly.  This means
-that the basic block of the returning function also needs to be stored in the
-stackframe, as that is the only assumption one can make when returning from a
-function.
-|*)
-
-  Variant step: state -> trace -> state -> Prop :=
-    | exec_bblock:
-      forall s f sp pc rs rs' m m' bb pr pr' t state,
-        f.(fn_code) ! pc = Some bb ->
-        step_instr_list sp (mk_instr_state rs pr m) bb.(bb_body)
-                           (mk_instr_state rs' pr' m') ->
-        step_cf_instr ge (State s f sp pc rs' pr' m') bb.(bb_exit) t state ->
-        step (State s f sp pc rs pr m) t state
-    | exec_function_internal:
-      forall s f args m m' stk bb cf,
-        Mem.alloc m 0 f.(fn_stacksize) = (m', stk) ->
-        f.(fn_code) ! (f.(fn_entrypoint)) = Some (mk_bblock bb cf) ->
-        step (Callstate s (Internal f) args m)
-             E0 (State s f
-                       (Vptr stk Ptrofs.zero)
-                       f.(fn_entrypoint)
-                       (init_regs args f.(fn_params))
-                       (PMap.init false)
-                       m')
-    | exec_function_external:
-      forall s ef args res t m m',
-        external_call ef ge args m t res m' ->
-        step (Callstate s (External ef) args m)
-             t (Returnstate s res m')
-    | exec_return:
-      forall res f sp pc rs s vres m pr,
-        step (Returnstate (Stackframe res f sp pc rs pr :: s) vres m)
-             E0 (State s f sp pc (rs#res <- vres) pr m).
-
-End RELSEM.
-
-Inductive initial_state (p: program): state -> Prop :=
-| initial_state_intro: forall b f m0,
-    let ge := Genv.globalenv p in
-    Genv.init_mem p = Some m0 ->
-    Genv.find_symbol ge p.(prog_main) = Some b ->
-    Genv.find_funct_ptr ge b = Some f ->
-    funsig f = signature_main ->
-    initial_state p (Callstate nil f nil m0).
-
-Inductive final_state: state -> int -> Prop :=
-| final_state_intro: forall r m,
-    final_state (Returnstate nil (Vint r) m) r.
-
-Definition semantics (p: program) :=
-  Semantics step (initial_state p) final_state (Genv.globalenv p).
diff --git a/src/hls/RTLBlockgen.v b/src/hls/RTLBlockgen.v
index cb18147..8f81e21 100644
--- a/src/hls/RTLBlockgen.v
+++ b/src/hls/RTLBlockgen.v
@@ -31,8 +31,8 @@ Require Import compcert.lib.Floats.
 
 Require Import vericert.common.DecEq.
 Require Import vericert.common.Vericertlib.
-Require Import vericert.hls.RTLBlockInstr.
-Require Import vericert.hls.RTLBlock.
+Require Import vericert.hls.Gible.
+Require Import vericert.hls.GibleSeq.
 
 #[local] Open Scope positive.
 
diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v
deleted file mode 100644
index e6aa002..0000000
--- a/src/hls/RTLPar.v
+++ /dev/null
@@ -1,119 +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/>.
- *)
-
-Require Import compcert.backend.Registers.
-Require Import compcert.common.AST.
-Require Import compcert.common.Events.
-Require Import compcert.common.Globalenvs.
-Require Import compcert.common.Memory.
-Require Import compcert.common.Smallstep.
-Require Import compcert.common.Values.
-Require Import compcert.lib.Coqlib.
-Require Import compcert.lib.Integers.
-Require Import compcert.lib.Maps.
-Require Import compcert.verilog.Op.
-
-Require Import vericert.hls.RTLBlockInstr.
-
-Definition bb := list (list (list instr)).
-
-Definition bblock := @bblock bb.
-Definition code := @code bb.
-Definition function := @function bb.
-Definition fundef := @fundef bb.
-Definition program := @program bb.
-Definition funsig := @funsig bb.
-Definition stackframe := @stackframe bb.
-Definition state := @state bb.
-Definition genv := @genv bb.
-
-Section RELSEM.
-
-  Context (ge: genv).
-
-  Definition step_instr_list := step_list (step_instr ge).
-  Definition step_instr_seq := step_list step_instr_list.
-  Definition step_instr_block := step_list step_instr_seq.
-
-  Variant step: state -> trace -> state -> Prop :=
-  | exec_bblock:
-    forall s f sp pc rs rs' m m' bb pr pr' state t,
-      f.(fn_code) ! pc = Some bb ->
-      step_instr_block sp (mk_instr_state rs pr m) bb.(bb_body)
-                          (mk_instr_state rs' pr' m') ->
-      step_cf_instr ge (State s f sp pc rs' pr' m') bb.(bb_exit) t state ->
-      step (State s f sp pc rs pr m) t state
-  | exec_function_internal:
-    forall s f args m m' stk bb cf,
-      Mem.alloc m 0 f.(fn_stacksize) = (m', stk) ->
-      f.(fn_code) ! (f.(fn_entrypoint)) = Some (mk_bblock bb cf) ->
-      step (Callstate s (Internal f) args m)
-        E0 (State s f
-                  (Vptr stk Ptrofs.zero)
-                  f.(fn_entrypoint)
-                  (init_regs args f.(fn_params))
-                  (PMap.init false)
-                  m')
-  | exec_function_external:
-    forall s ef args res t m m',
-      external_call ef ge args m t res m' ->
-      step (Callstate s (External ef) args m)
-           t (Returnstate s res m')
-  | exec_return:
-    forall res f sp pc rs s vres m pr,
-      step (Returnstate (Stackframe res f sp pc rs pr :: s) vres m)
-        E0 (State s f sp pc (rs#res <- vres) pr m).
-
-End RELSEM.
-
-Inductive initial_state (p: program): state -> Prop :=
-  | initial_state_intro: forall b f m0,
-      let ge := Genv.globalenv p in
-      Genv.init_mem p = Some m0 ->
-      Genv.find_symbol ge p.(prog_main) = Some b ->
-      Genv.find_funct_ptr ge b = Some f ->
-      funsig f = signature_main ->
-      initial_state p (Callstate nil f nil m0).
-
-Inductive final_state: state -> int -> Prop :=
-  | final_state_intro: forall r m,
-      final_state (Returnstate nil (Vint r) m) r.
-
-Definition semantics (p: program) :=
-  Semantics step (initial_state p) final_state (Genv.globalenv p).
-
-Definition max_reg_bblock (m : positive) (pc : node) (bb : bblock) :=
-  let max_body :=
-    fold_left
-      (fun x l => fold_left (fun x' l' => fold_left max_reg_instr l' x') l x)
-      bb.(bb_body) m
-  in
-  max_reg_cfi max_body bb.(bb_exit).
-
-Definition max_reg_function (f: function) :=
-  Pos.max
-    (PTree.fold max_reg_bblock f.(fn_code) 1%positive)
-    (fold_left Pos.max f.(fn_params) 1%positive).
-
-Definition max_pc_function (f: function) : positive :=
-  PTree.fold
-    (fun m pc i =>
-       (Pos.max m
-                (pc + match Zlength i.(bb_body)
-                      with Z.pos p => p | _ => 1 end))%positive)
-    f.(fn_code) 1%positive.