Add more sub languages

4 files changed, 608 insertions, 1 deletions

diff --git a/src/Compiler.v b/src/Compiler.v
index a539c1c..c568374 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -64,7 +64,9 @@ Require vericert.hls.HTLgen.
 Require vericert.hls.GibleSeq.
 Require vericert.hls.GibleSeqgen.
 Require vericert.hls.GiblePargen.
+Require vericert.hls.GibleSubPargen.
 Require vericert.hls.HTLPargen.
+Require vericert.hls.DHTLgen.
 Require vericert.hls.DVeriloggen.
 (*Require vericert.hls.Pipeline.*)
 Require vericert.hls.IfConversion.
@@ -296,7 +298,9 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program :=
    @@ print (print_GibleSeq 5)
   @@@ time "Scheduling" GiblePargen.transl_program
    @@ print (print_GiblePar 0)
-  @@@ HTLPargen.transl_program
+  @@@ GibleSubPargen.transl_program
+  (* @@@ HTLPargen.transl_program *)
+  @@@ DHTLgen.transl_program
    @@ print (print_DHTL 0)
    @@ ClockMemory.transf_program
    @@ print (print_DHTL 1)
diff --git a/src/hls/DHTLgen.v b/src/hls/DHTLgen.v
new file mode 100644
index 0000000..4b931c7
--- /dev/null
+++ b/src/hls/DHTLgen.v
@@ -0,0 +1,465 @@
+(* 
+ * Vericert: Verified high-level synthesis.
+ * Copyright (C) 2023 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 Coq.micromega.Lia.
+
+Require Import compcert.lib.Maps.
+Require Import compcert.common.Errors.
+Require compcert.common.Globalenvs.
+Require compcert.lib.Integers.
+Require Import compcert.common.AST.
+
+Require Import vericert.common.Statemonad.
+Require Import vericert.common.Vericertlib.
+Require Import vericert.hls.AssocMap.
+Require Import vericert.hls.DHTL.
+Require Import vericert.hls.ValueInt.
+Require Import vericert.hls.Verilog.
+Require Import vericert.hls.Gible.
+Require Import vericert.hls.GibleSubPar.
+Require Import vericert.hls.Predicate.
+Require Import vericert.common.Errormonad.
+Import ErrorMonad.
+Import ErrorMonadExtra.
+Import MonadNotation.
+
+#[local] Open Scope monad_scope.
+
+#[local] Hint Resolve AssocMap.gempty : htlh.
+#[local] Hint Resolve AssocMap.gso : htlh.
+#[local] Hint Resolve AssocMap.gss : htlh.
+#[local] Hint Resolve Ple_refl : htlh.
+#[local] Hint Resolve Ple_succ : htlh.
+
+Record control_regs: Type := mk_control_regs {
+  ctrl_st : reg;
+  ctrl_stack : reg;
+  ctrl_fin : reg;
+  ctrl_return : reg;
+}.
+
+(* Definition pred_lit (preg: reg) (pred: predicate) := *)
+(*   Vrange preg (Vlit (posToValue pred)) (Vlit (posToValue pred)). *)
+
+(* Fixpoint pred_expr (preg: reg) (p: pred_op) := *)
+(*   match p with *)
+(*   | Plit (b, pred) => *)
+(*     if b *)
+(*     then pred_lit preg pred *)
+(*     else Vunop Vnot (pred_lit preg pred) *)
+(*   | Ptrue => Vlit (ZToValue 1) *)
+(*   | Pfalse => Vlit (ZToValue 0) *)
+(*   | Pand p1 p2 => *)
+(*     Vbinop Vand (pred_expr preg p1) (pred_expr preg p2) *)
+(*   | Por p1 p2 => *)
+(*     Vbinop Vor (pred_expr preg p1) (pred_expr preg p2) *)
+(*   end. *)
+
+Definition pred_enc (pred: predicate) :=
+  xI pred.
+
+Definition reg_enc (r: reg) :=
+  xO r.
+
+Fixpoint pred_expr (p: pred_op) :=
+  match p with
+  | Plit (b, pred) =>
+    if b
+    then Vvar (pred_enc pred)
+    else (Vbinop Veq (Vvar (pred_enc pred)) (Vlit Integers.Int.zero))
+  | Ptrue => Vlit (boolToValue true)
+  | Pfalse => Vlit (boolToValue false)
+  | Pand p1 p2 =>
+    Vbinop Vand (pred_expr p1) (pred_expr p2)
+  | Por p1 p2 =>
+    Vbinop Vor (pred_expr p1) (pred_expr p2)
+  end.
+
+Definition assignment : Type := expr -> expr -> stmnt.
+
+Definition translate_predicate (a : assignment)
+           (p: option pred_op) (dst e: expr) :=
+  match p with
+  | None => a dst e
+  | Some pos =>
+    let pos' := deep_simplify peq pos in
+    match sat_pred_simple (negate pos') with
+    | None => a dst e
+    | Some _ => a dst (Vternary (pred_expr pos') e dst)
+    end
+  end.
+ 
+Definition state_goto (p: option pred_op) (st : reg) (n : node) : stmnt :=
+  translate_predicate Vblock p (Vvar st) (Vlit (posToValue n)).
+
+Definition state_cond (p: option pred_op) (st : reg) (c : expr) (n1 n2 : node) : stmnt :=
+  translate_predicate Vblock p (Vvar st) (Vternary c (posToExpr n1) (posToExpr n2)).
+
+Definition nonblock (dst : reg) (e : expr) := Vnonblock (Vvar (reg_enc dst)) e.
+Definition block (dst : reg) (e : expr) := Vblock (Vvar (reg_enc dst)) e.
+
+Definition bop (op : binop) (r1 r2 : reg) : expr :=
+  Vbinop op (Vvar (reg_enc r1)) (Vvar (reg_enc r2)).
+
+Definition boplit (op : binop) (r : reg) (l : Integers.int) : expr :=
+  Vbinop op (Vvar (reg_enc r)) (Vlit (intToValue l)).
+
+Definition boplitz (op: binop) (r: reg) (l: Z) : expr :=
+  Vbinop op (Vvar (reg_enc r)) (Vlit (ZToValue l)).
+
+Definition error {A} m := @Errors.Error A (Errors.msg m).
+
+Definition translate_comparison (c : Integers.comparison) (args : list reg) : Errors.res expr :=
+  match c, args with
+  | Integers.Ceq, r1::r2::nil => ret (bop Veq r1 r2)
+  | Integers.Cne, r1::r2::nil => ret (bop Vne r1 r2)
+  | Integers.Clt, r1::r2::nil => ret (bop Vlt r1 r2)
+  | Integers.Cgt, r1::r2::nil => ret (bop Vgt r1 r2)
+  | Integers.Cle, r1::r2::nil => ret (bop Vle r1 r2)
+  | Integers.Cge, r1::r2::nil => ret (bop Vge r1 r2)
+  | _, _ => error "Htlpargen: comparison instruction not implemented: other"
+  end.
+
+Definition translate_comparison_imm (c : Integers.comparison) (args : list reg) (i: Integers.int)
+  : Errors.res expr :=
+  match c, args with
+  | Integers.Ceq, r1::nil => Errors.OK (boplit Veq r1 i)
+  | Integers.Cne, r1::nil => Errors.OK (boplit Vne r1 i)
+  | Integers.Clt, r1::nil => Errors.OK (boplit Vlt r1 i)
+  | Integers.Cgt, r1::nil => Errors.OK (boplit Vgt r1 i)
+  | Integers.Cle, r1::nil => Errors.OK (boplit Vle r1 i)
+  | Integers.Cge, r1::nil => Errors.OK (boplit Vge r1 i)
+  | _, _ => error "Htlpargen: comparison_imm instruction not implemented: other"
+  end.
+
+Definition translate_comparisonu (c : Integers.comparison) (args : list reg) : Errors.res expr :=
+  match c, args with
+  | Integers.Clt, r1::r2::nil => Errors.OK (bop Vltu r1 r2)
+  | Integers.Cgt, r1::r2::nil => Errors.OK (bop Vgtu r1 r2)
+  | Integers.Cle, r1::r2::nil => Errors.OK (bop Vleu r1 r2)
+  | Integers.Cge, r1::r2::nil => Errors.OK (bop Vgeu r1 r2)
+  | _, _ => Errors.Error (Errors.msg "Htlpargen: comparison instruction not implemented: other")
+  end.
+
+Definition translate_comparison_immu (c : Integers.comparison) (args : list reg) (i: Integers.int)
+  : Errors.res expr :=
+  match c, args with
+  | Integers.Clt, r1::nil => Errors.OK (boplit Vltu r1 i)
+  | Integers.Cgt, r1::nil => Errors.OK (boplit Vgtu r1 i)
+  | Integers.Cle, r1::nil => Errors.OK (boplit Vleu r1 i)
+  | Integers.Cge, r1::nil => Errors.OK (boplit Vgeu r1 i)
+  | _, _ => Errors.Error (Errors.msg "Htlpargen: comparison_imm instruction not implemented: other")
+  end.
+
+Definition translate_condition (c : Op.condition) (args : list reg) : Errors.res expr :=
+  match c, args with
+  | Op.Ccomp c, _ => translate_comparison c args
+  | Op.Ccompu c, _ => translate_comparisonu c args
+  | Op.Ccompimm c i, _ => translate_comparison_imm c args i
+  | Op.Ccompuimm c i, _ => translate_comparison_immu c args i
+  | Op.Cmaskzero n, _ => Errors.Error (Errors.msg "Htlpargen: condition instruction not implemented: Cmaskzero")
+  | Op.Cmasknotzero n, _ => Errors.Error (Errors.msg "Htlpargen: condition instruction not implemented: Cmasknotzero")
+  | _, _ => Errors.Error (Errors.msg "Htlpargen: condition instruction not implemented: other")
+  end.
+
+Definition check_address_parameter_signed (p : Z) : bool :=
+  Z.leb Integers.Ptrofs.min_signed p
+  && Z.leb p Integers.Ptrofs.max_signed.
+
+Definition check_address_parameter_unsigned (p : Z) : bool :=
+  Z.leb p Integers.Ptrofs.max_unsigned.
+
+Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : Errors.res expr :=
+  match a, args with (* TODO: We should be more methodical here; what are the possibilities?*)
+  | Op.Aindexed off, r1::nil =>
+    if (check_address_parameter_signed off)
+    then Errors.OK (boplitz Vadd r1 off)
+    else Errors.Error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed): address out of bounds")
+  | Op.Ascaled scale offset, r1::nil =>
+    if (check_address_parameter_signed scale) && (check_address_parameter_signed offset)
+    then Errors.OK (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue offset)))
+    else Errors.Error (Errors.msg "Veriloggen: translate_eff_addressing (Ascaled): address out of bounds")
+  | Op.Aindexed2 offset, r1::r2::nil =>
+    if (check_address_parameter_signed offset)
+    then Errors.OK (Vbinop Vadd (bop Vadd r1 r2) (Vlit (ZToValue offset)))
+    else Errors.Error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2): address out of bounds")
+  | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)
+    if (check_address_parameter_signed scale) && (check_address_parameter_signed offset)
+    then Errors.OK (Vbinop Vadd (Vvar (reg_enc r1)) (Vbinop Vadd (boplitz Vmul r2 scale) (Vlit (ZToValue offset))))
+    else Errors.Error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2scaled): address out of bounds")
+  | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)
+    let a := Integers.Ptrofs.unsigned a in
+    if (check_address_parameter_unsigned a)
+    then Errors.OK (Vlit (ZToValue a))
+    else Errors.Error (Errors.msg "Veriloggen: translate_eff_addressing (Ainstack): address out of bounds")
+  | _, _ => Errors.Error (Errors.msg "Veriloggen: translate_eff_addressing unsuported addressing")
+  end.
+
+#[local] Close Scope monad_scope.
+#[local] Open Scope error_monad_scope.
+
+(** Translate an instruction to a statement. FIX mulhs mulhu *)
+Definition translate_instr (op : Op.operation) (args : list reg) : Errors.res expr :=
+  match op, args with
+  | Op.Omove, r::nil => Errors.OK (Vvar (reg_enc r))
+  | Op.Ointconst n, _ => Errors.OK (Vlit (intToValue n))
+  | Op.Oneg, r::nil => Errors.OK (Vunop Vneg (Vvar (reg_enc r)))
+  | Op.Osub, r1::r2::nil => Errors.OK (bop Vsub r1 r2)
+  | Op.Omul, r1::r2::nil => Errors.OK (bop Vmul r1 r2)
+  | Op.Omulimm n, r::nil => Errors.OK (boplit Vmul r n)
+  | Op.Omulhs, r1::r2::nil => Errors.Error (Errors.msg "Htlpargen: Instruction not implemented: mulhs")
+  | Op.Omulhu, r1::r2::nil => Errors.Error (Errors.msg "Htlpargen: Instruction not implemented: mulhu")
+  | Op.Odiv, r1::r2::nil => Errors.OK (bop Vdiv r1 r2)
+  | Op.Odivu, r1::r2::nil => Errors.OK (bop Vdivu r1 r2)
+  | Op.Omod, r1::r2::nil => Errors.OK (bop Vmod r1 r2)
+  | Op.Omodu, r1::r2::nil => Errors.OK (bop Vmodu r1 r2)
+  | Op.Oand, r1::r2::nil => Errors.OK (bop Vand r1 r2)
+  | Op.Oandimm n, r::nil => Errors.OK (boplit Vand r n)
+  | Op.Oor, r1::r2::nil => Errors.OK (bop Vor r1 r2)
+  | Op.Oorimm n, r::nil => Errors.OK (boplit Vor r n)
+  | Op.Oxor, r1::r2::nil => Errors.OK (bop Vxor r1 r2)
+  | Op.Oxorimm n, r::nil => Errors.OK (boplit Vxor r n)
+  | Op.Onot, r::nil => Errors.OK (Vunop Vnot (Vvar (reg_enc r)))
+  | Op.Oshl, r1::r2::nil => Errors.OK (bop Vshl r1 r2)
+  | Op.Oshlimm n, r::nil => Errors.OK (boplit Vshl r n)
+  | Op.Oshr, r1::r2::nil => Errors.OK (bop Vshr r1 r2)
+  | Op.Oshrimm n, r::nil => Errors.OK (boplit Vshr r n)
+  | Op.Oshrximm n, r::nil =>
+    Errors.OK (Vternary (Vbinop Vlt (Vvar (reg_enc r)) (Vlit (ZToValue 0)))
+                  (Vunop Vneg (Vbinop Vshru (Vunop Vneg (Vvar (reg_enc r))) (Vlit n)))
+                  (Vbinop Vshru (Vvar (reg_enc r)) (Vlit n)))
+  | Op.Oshru, r1::r2::nil => Errors.OK (bop Vshru r1 r2)
+  | Op.Oshruimm n, r::nil => Errors.OK (boplit Vshru r n)
+  | Op.Ororimm n, r::nil => Errors.Error (Errors.msg "Htlpargen: Instruction not implemented: Ororimm")
+  (*Errors.OK (Vbinop Vor (boplit Vshru r (Integers.Int.modu n (Integers.Int.repr 32)))
+                                        (boplit Vshl r (Integers.Int.sub (Integers.Int.repr 32) (Integers.Int.modu n (Integers.Int.repr 32)))))*)
+  | Op.Oshldimm n, r::nil => Errors.OK (Vbinop Vor (boplit Vshl r n) (boplit Vshr r (Integers.Int.sub (Integers.Int.repr 32) n)))
+  | Op.Ocmp c, _ => translate_condition c args
+  | Op.Osel c AST.Tint, r1::r2::rl =>
+    do tc <- translate_condition c rl;
+    Errors.OK (Vternary tc (Vvar (reg_enc r1)) (Vvar (reg_enc r2)))
+  | Op.Olea a, _ => translate_eff_addressing a args
+  | _, _ => Errors.Error (Errors.msg "Htlpargen: Instruction not implemented: other")
+  end.
+
+Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing)
+           (args : list reg) (stack : reg) : Errors.res expr :=
+  match mem, addr, args with (* TODO: We should be more methodical here; what are the possibilities?*)
+  | Mint32, Op.Aindexed off, r1::nil =>
+    if (check_address_parameter_signed off)
+    then Errors.OK (Vvari stack (Vbinop Vdivu (boplitz Vadd r1 off) (Vlit (ZToValue 4))))
+    else Errors.Error (Errors.msg "HTLPargen: translate_arr_access address out of bounds")
+  | Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)
+    if (check_address_parameter_signed scale) && (check_address_parameter_signed offset)
+    then Errors.OK (Vvari stack
+                    (Vbinop Vdivu
+                            (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale))
+                            (Vlit (ZToValue 4))))
+    else Errors.Error (Errors.msg "HTLPargen: translate_arr_access address out of bounds")
+  | Mint32, Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)
+    let a := Integers.Ptrofs.unsigned a in
+    if (check_address_parameter_unsigned a)
+    then Errors.OK (Vvari stack (Vlit (ZToValue (a / 4))))
+    else Errors.Error (Errors.msg "HTLPargen: eff_addressing out of bounds stack offset")
+  | _, _, _ => Errors.Error (Errors.msg "HTLPargen: translate_arr_access unsuported addressing")
+  end.
+
+Fixpoint enumerate (i : nat) (ns : list node) {struct ns} : list (nat * node) :=
+  match ns with
+  | n :: ns' => (i, n) :: enumerate (i+1) ns'
+  | nil => nil
+  end.
+
+Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) :=
+  List.map (fun a => match a with
+                    (i, n) => (Vlit (natToValue i), Vblock (Vvar st) (Vlit (posToValue n)))
+                  end)
+           (enumerate 0 ns).
+
+Definition translate_cfi (ctrl: control_regs) p (cfi: cf_instr)
+  : Errors.res stmnt :=
+  match cfi with
+  | RBgoto n' =>
+    Errors.OK (state_goto p ctrl.(ctrl_st) n')
+  | RBcond c args n1 n2 =>
+    do e <- translate_condition c args;
+    Errors.OK (state_cond p ctrl.(ctrl_st) e n1 n2)
+  | RBreturn r =>
+    match r with
+    | Some r' =>
+      Errors.OK (Vseq (block ctrl.(ctrl_fin) (Vlit (ZToValue 1%Z))) (block ctrl.(ctrl_return) (Vvar r')))
+    | None =>
+      Errors.OK (Vseq (block ctrl.(ctrl_fin) (Vlit (ZToValue 1%Z))) (block ctrl.(ctrl_return) (Vlit (ZToValue 0%Z))))
+    end
+  | RBjumptable r tbl =>
+    Errors.OK (Vcase (Vvar r) (list_to_stmnt (tbl_to_case_expr ctrl.(ctrl_st) tbl)) (Some Vskip))
+  | RBcall sig ri rl r n =>
+    Errors.Error (Errors.msg "HTLPargen: RBcall not supported.")
+  | RBtailcall sig ri lr =>
+    Errors.Error (Errors.msg "HTLPargen: RBtailcall not supported.")
+  | RBbuiltin e lb b n =>
+    Errors.Error (Errors.msg "HTLPargen: RBbuildin not supported.")
+  end.
+
+Definition transf_instr (ctrl: control_regs) (dc: pred_op * stmnt) (i: instr)
+           : Errors.res (pred_op * stmnt) :=
+  let '(curr_p, d) := dc in
+  let npred p := Some (Pand curr_p (dfltp p)) in
+  match i with
+  | RBnop => Errors.OK dc
+  | RBop p op args dst => 
+    do instr <- translate_instr op args;
+    let stmnt := translate_predicate Vblock (npred p) (Vvar dst) instr in
+    Errors.OK (curr_p, Vseq d stmnt)
+  | RBload p mem addr args dst =>
+    do src <- translate_arr_access mem addr args ctrl.(ctrl_stack);
+    let stmnt := translate_predicate Vblock (npred p) (Vvar dst) src in
+    Errors.OK (curr_p, Vseq d stmnt)
+  | RBstore p mem addr args src =>
+    do dst <- translate_arr_access mem addr args ctrl.(ctrl_stack);
+    let stmnt := translate_predicate Vblock (npred p) dst (Vvar src) in
+    Errors.OK (curr_p, Vseq d stmnt)
+  | RBsetpred p' cond args p =>
+    do cond' <- translate_condition cond args;
+    let stmnt := translate_predicate Vblock (npred p') (pred_expr (Plit (true, p))) cond' in
+    Errors.OK (curr_p, Vseq d stmnt)
+  | RBexit p cf => 
+    do d_stmnt <- translate_cfi ctrl (npred p) cf;
+    Errors.OK (Pand curr_p (negate (dfltp p)), Vseq d d_stmnt)
+  end.
+
+Definition transf_chained_block (ctrl: control_regs) (dc: @pred_op positive * stmnt) (block: list instr)
+           : Errors.res (pred_op * stmnt) :=
+  mfold_left (transf_instr ctrl) block (OK dc).
+
+Definition transf_parallel_block (ctrl: control_regs) (block: list (list instr))
+           : Errors.res (pred_op * stmnt) :=
+  mfold_left (transf_chained_block ctrl) block (OK (Ptrue, Vskip)).
+
+Definition transf_seq_block (ctrl: control_regs) (d: datapath) (ni: node * SubParBB.t)
+           : Errors.res datapath :=
+  let (n, bb) := ni in
+  match d ! n with
+  | None => 
+    do (_pred, stmnt) <- transf_parallel_block ctrl bb;
+    OK (PTree.set n stmnt d)
+  | _ => Error (msg "DHTLgen: overwriting location")
+  end.
+
+Definition stack_correct (sz : Z) : bool :=
+  (0 <=? sz) && (sz <? Integers.Ptrofs.modulus) && (Z.modulo sz 4 =? 0).
+
+Definition max_pc_map (m : Maps.PTree.t stmnt) :=
+  PTree.fold (fun m pc i => Pos.max m pc) m 1%positive.
+
+Lemma max_pc_map_sound:
+  forall m pc i, m!pc = Some i -> Ple pc (max_pc_map m).
+Proof.
+  intros until i. unfold max_pc_function.
+  apply PTree_Properties.fold_rec with (P := fun c m => c!pc = Some i -> Ple pc m).
+  (* extensionality *)
+  intros. apply H0. rewrite H; auto.
+  (* base case *)
+  rewrite PTree.gempty. congruence.
+  (* inductive case *)
+  intros. rewrite PTree.gsspec in H2. destruct (peq pc k).
+  inv H2. unfold Ple; lia.
+  apply Ple_trans with a. auto. unfold Ple; lia.
+Qed.
+
+Lemma max_pc_wf :
+  forall m, Z.pos (max_pc_map m) <= Integers.Int.max_unsigned ->
+            map_well_formed m.
+Proof.
+  unfold map_well_formed. intros.
+  exploit list_in_map_inv. eassumption. intros [x [A B]]. destruct x.
+  apply Maps.PTree.elements_complete in B. apply max_pc_map_sound in B.
+  unfold Ple in B. apply Pos2Z.pos_le_pos in B. subst.
+  simplify. transitivity (Z.pos (max_pc_map m)); eauto.
+Qed.
+
+Definition decide_order a b c d e f g : {module_ordering a b c d e f g} + {True}.
+  refine (match bool_dec ((a <? b) && (b <? c) && (c <? d)
+                          && (d <? e) && (e <? f) && (f <? g))%positive true with
+          | left t => left _
+          | _ => _
+          end); auto.
+  simplify; repeat match goal with
+                   | H: context[(_ <? _)%positive] |- _ => apply Pos.ltb_lt in H
+                   end; unfold module_ordering; auto.
+Defined.
+
+Definition max_resource_function (f: function) :=
+  Pos.max (reg_enc (max_reg_function f)) (pred_enc (max_pred_function f)).
+
+Program Definition transl_module (f: function) : res DHTL.module :=
+  if stack_correct f.(fn_stacksize) then
+    let st := Pos.succ (max_resource_function f) in
+    let fin := Pos.succ st in
+    let rtrn := Pos.succ fin in
+    let stack := Pos.succ rtrn in
+    let start := Pos.succ stack in
+    let rst := Pos.succ start in
+    let clk := Pos.succ rst in
+    do _stmnt <- mfold_left (transf_seq_block (mk_control_regs st stack fin rtrn)) 
+                            (Maps.PTree.elements f.(GibleSubPar.fn_code)) (ret (PTree.empty _));
+    match zle (Z.pos (max_pc_map _stmnt)) Integers.Int.max_unsigned,
+            decide_order st fin rtrn stack start rst clk,
+            max_list_dec (List.map reg_enc (GibleSubPar.fn_params f)) st
+    with
+    | left LEDATA, left MORD, left WFPARAMS =>
+        ret (DHTL.mkmodule
+           (List.map reg_enc f.(GibleSubPar.fn_params))
+           _stmnt
+           f.(fn_entrypoint)
+           st
+           stack
+           (Z.to_nat (f.(fn_stacksize) / 4))
+           fin
+           rtrn
+           start
+           rst
+           clk
+           (AssocMap.empty _)
+           (AssocMap.empty _)
+           None
+           (max_pc_wf _ LEDATA)
+           MORD
+           _
+           WFPARAMS)
+    | _, _, _ => error "More than 2^32 states"
+    end
+  else error "Stack size misalignment".
+
+Definition transl_fundef := transf_partial_fundef transl_module.
+
+Definition main_is_internal (p : GibleSubPar.program) : bool :=
+  let ge := Globalenvs.Genv.globalenv p in
+  match Globalenvs.Genv.find_symbol ge p.(AST.prog_main) with
+  | Some b =>
+    match Globalenvs.Genv.find_funct_ptr ge b with
+    | Some (AST.Internal _) => true
+    | _ => false
+    end
+  | _ => false
+  end.
+
+Definition transl_program (p : GibleSubPar.program) : Errors.res DHTL.program :=
+  if main_is_internal p
+  then transform_partial_program transl_fundef p
+  else Errors.Error (Errors.msg "Main function is not Internal").
diff --git a/src/hls/GibleSubPar.v b/src/hls/GibleSubPar.v
new file mode 100644
index 0000000..c867e1b
--- /dev/null
+++ b/src/hls/GibleSubPar.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.
+
+(*|
+=========
+Gible Seq
+=========
+|*)
+
+Module SubParBB <: BlockType.
+
+  Definition t := list (list instr).
+
+  Definition foldl (A: Type) (f: A -> instr -> A) (bb : t) (m : A): A :=
+    fold_left
+      (fun x l => fold_left f l x)
+      bb m.
+
+  Definition length : t -> nat := @length (list instr).
+
+  Section RELSEM.
+
+    Context {A B: Type} (ge: Genv.t A B).
+
+    Definition step_instr_list := step_list_inter (step_instr ge).
+    Definition step_instr_seq := step_list step_instr_list.
+
+(*|
+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_seq.
+
+  End RELSEM.
+
+End SubParBB.
+
+Module GibleSubPar := Gible(SubParBB).
+Export GibleSubPar.
diff --git a/src/hls/GibleSubPargen.v b/src/hls/GibleSubPargen.v
new file mode 100644
index 0000000..a6dfa4a
--- /dev/null
+++ b/src/hls/GibleSubPargen.v
@@ -0,0 +1,63 @@
+(* 
+ * Vericert: Verified high-level synthesis.
+ * Copyright (C) 2023 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 Coq.micromega.Lia.
+
+Require Import compcert.lib.Maps.
+Require Import compcert.common.Errors.
+Require compcert.common.Globalenvs.
+Require compcert.lib.Integers.
+Require Import compcert.common.AST.
+
+Require Import vericert.common.Statemonad.
+Require Import vericert.common.Vericertlib.
+Require Import vericert.hls.AssocMap.
+Require Import vericert.hls.ValueInt.
+Require Import vericert.hls.Verilog.
+Require Import vericert.hls.Gible.
+Require Import vericert.hls.GibleSubPar.
+Require Import vericert.hls.GiblePar.
+Require Import vericert.hls.Predicate.
+Require Import vericert.common.Errormonad.
+Import ErrorMonad.
+Import ErrorMonadExtra.
+Import MonadNotation.
+
+#[local] Open Scope monad_scope.
+
+Definition transl_block' (icode: positive * (positive * GibleSubPar.code)) (bb: SubParBB.t): 
+  res (positive * (positive * GibleSubPar.code)) :=
+  let '(curr, (next, code)) := icode in
+  match code ! curr with
+  | None => OK (next, (Pos.succ next, PTree.set curr (bb ++ (((RBexit None (RBgoto next))::nil)::nil)) code))
+  | _ => Error (msg "GibleSubPargen: Overlapping blocks in translation")
+  end.
+
+Definition transl_block (freshcode: positive * GibleSubPar.code) (ibb: positive * ParBB.t): res (positive * GibleSubPar.code) :=
+  let (i, bb) := ibb in
+  let (fresh, code) := freshcode in
+  map snd (mfold_left transl_block' bb (OK (i, (fresh, code)))).
+
+Definition transl_function (f: GiblePar.function) : res GibleSubPar.function :=
+  do new_code <- mfold_left transl_block (PTree.elements f.(fn_code)) (OK (Pos.succ (max_pc_function f), PTree.empty _));
+  OK (GibleSubPar.mkfunction f.(fn_sig) f.(fn_params) f.(fn_stacksize) (snd new_code) f.(fn_entrypoint)).
+
+Definition transl_fundef := transf_partial_fundef transl_function.
+
+Definition transl_program (p : GiblePar.program) : Errors.res GibleSubPar.program :=
+  transform_partial_program transl_fundef p.