Add beginning to memory generation proof

1 files changed, 334 insertions, 634 deletions

diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v
index b602ab6..10c4357 100644
--- a/src/hls/HTLPargen.v
+++ b/src/hls/HTLPargen.v
@@ -1,6 +1,7 @@
-(*
+(* 
  * Vericert: Verified high-level synthesis.
- * Copyright (C) 2021 Yann Herklotz <yann@yannherklotz.com>
+ * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
+ *               2020 James Pollard <j@mes.dev>
  *
  * 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
@@ -18,23 +19,21 @@
 
 Require Import Coq.micromega.Lia.
 
-Require Import compcert.common.AST.
-Require compcert.common.Errors.
+Require Import compcert.lib.Maps.
+Require Import compcert.common.Errors.
 Require compcert.common.Globalenvs.
 Require compcert.lib.Integers.
-Require Import compcert.lib.Maps.
+Require Import compcert.common.AST.
 
 Require Import vericert.common.Statemonad.
 Require Import vericert.common.Vericertlib.
 Require Import vericert.hls.AssocMap.
-Require Import vericert.hls.FunctionalUnits.
-Require Import vericert.hls.HTL.
-Require Import vericert.hls.Predicate.
-Require Import vericert.hls.GiblePar.
-Require Import vericert.hls.Gible.
-Require Import vericert.hls.FunctionalUnits.
+Require Import vericert.hls.DHTL.
 Require Import vericert.hls.ValueInt.
 Require Import vericert.hls.Verilog.
+Require Import vericert.hls.Gible.
+Require Import vericert.hls.GiblePar.
+Require Import vericert.hls.Predicate.
 
 #[local] Hint Resolve AssocMap.gempty : htlh.
 #[local] Hint Resolve AssocMap.gso : htlh.
@@ -42,16 +41,13 @@ Require Import vericert.hls.Verilog.
 #[local] Hint Resolve Ple_refl : htlh.
 #[local] Hint Resolve Ple_succ : htlh.
 
-Definition assignment : Type := expr -> expr -> stmnt.
-
 Record state: Type := mkstate {
-  st_st: reg;
+  st_st : reg;
   st_freshreg: reg;
   st_freshstate: node;
   st_scldecls: AssocMap.t (option io * scl_decl);
   st_arrdecls: AssocMap.t (option io * arr_decl);
   st_datapath: datapath;
-  st_controllogic: controllogic;
 }.
 
 Definition init_state (st : reg) : state :=
@@ -60,7 +56,6 @@ Definition init_state (st : reg) : state :=
           1%positive
           (AssocMap.empty (option io * scl_decl))
           (AssocMap.empty (option io * arr_decl))
-          (AssocMap.empty stmnt)
           (AssocMap.empty stmnt).
 
 Module HTLState <: State.
@@ -74,23 +69,20 @@ Module HTLState <: State.
         Ple s1.(st_freshreg) s2.(st_freshreg) ->
         Ple s1.(st_freshstate) s2.(st_freshstate) ->
         (forall n,
-            s1.(st_controllogic)!n = None
-            \/ s2.(st_controllogic)!n = s1.(st_controllogic)!n) ->
+            s1.(st_datapath)!n = None \/ s2.(st_datapath)!n = s1.(st_datapath)!n) ->
         st_incr s1 s2.
-  #[local] Hint Constructors st_incr : htlh.
+  #[export] Hint Constructors st_incr : htlh.
 
   Definition st_prop := st_incr.
-  #[local] Hint Unfold st_prop : htlh.
+  #[export] Hint Unfold st_prop : htlh.
 
-  Lemma st_refl : forall s, st_prop s s.
-  Proof. auto with htlh. Qed.
+  Lemma st_refl : forall s, st_prop s s. Proof. auto with htlh. Qed.
 
   Lemma st_trans :
     forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3.
   Proof.
-    intros. inv H. inv H0.
-    apply state_incr_intro; eauto using Ple_trans; intros; try congruence.
-    destruct H4 with n; destruct H7 with n; intuition congruence.
+    intros. inv H. inv H0. apply state_incr_intro; eauto using Ple_trans; intros; try congruence.
+    - destruct H4 with n; destruct H7 with n; intuition congruence.
   Qed.
 
 End HTLState.
@@ -102,14 +94,18 @@ Export HTLMonad.
 Module HTLMonadExtra := Monad.MonadExtra(HTLMonad).
 Import HTLMonadExtra.
 Export MonadNotation.
+
 #[local] Open Scope monad_scope.
 
+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 Vrange preg (Vlit (posToValue pred)) (Vlit (posToValue pred))
-    else Vunop Vnot (Vrange preg (Vlit (posToValue pred)) (Vlit (posToValue pred)))
+    then pred_lit preg pred
+    else Vunop Vnot (pred_lit preg pred)
   | Ptrue => Vlit (ZToValue 1)
   | Pfalse => Vlit (ZToValue 0)
   | Pand p1 p2 =>
@@ -118,14 +114,20 @@ Fixpoint pred_expr (preg: reg) (p: pred_op) :=
     Vbinop Vor (pred_expr preg p1) (pred_expr preg p2)
   end.
 
+Definition assignment : Type := expr -> expr -> stmnt.
+
 Definition translate_predicate (a : assignment)
            (preg: reg) (p: option pred_op) (dst e: expr) :=
   match p with
   | None => a dst e
   | Some pos =>
-    a dst (Vternary (pred_expr preg pos) e dst)
+    let pos' := deep_simplify peq pos in
+    match sat_pred_simple (negate pos') with
+    | None => a dst e
+    | Some _ => a dst (Vternary (pred_expr preg pos') e dst)
+    end
   end.
-
+ 
 Definition state_goto (preg: reg) (p: option pred_op) (st : reg) (n : node) : stmnt :=
   translate_predicate Vblock preg p (Vvar st) (Vlit (posToValue n)).
 
@@ -138,11 +140,11 @@ Proof.
   intros. case (s.(st_datapath)!n); tauto.
 Defined.
 
-Definition check_empty_node_controllogic:
-  forall (s: state) (n: node), { s.(st_controllogic)!n = None } + { True }.
-Proof.
-  intros. case (s.(st_controllogic)!n); tauto.
-Defined.
+Definition append_instr (n : node) (st : stmnt) (d : datapath) : datapath :=
+  match AssocMap.get n d with 
+  | Some st' => AssocMap.set n (Vseq st' st) d
+  | None => AssocMap.set n st d
+  end.
 
 Lemma declare_reg_state_incr :
   forall i s r sz,
@@ -153,8 +155,7 @@ Lemma declare_reg_state_incr :
        s.(st_freshstate)
        (AssocMap.set r (i, VScalar sz) s.(st_scldecls))
        s.(st_arrdecls)
-       s.(st_datapath)
-       s.(st_controllogic)).
+       s.(st_datapath)).
 Proof. Admitted.
 
 Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit :=
@@ -164,8 +165,7 @@ Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit :=
                 s.(st_freshstate)
                 (AssocMap.set r (i, VScalar sz) s.(st_scldecls))
                 s.(st_arrdecls)
-                s.(st_datapath)
-                s.(st_controllogic))
+                s.(st_datapath))
               (declare_reg_state_incr i s r sz).
 
 Lemma declare_arr_state_incr :
@@ -177,8 +177,7 @@ Lemma declare_arr_state_incr :
        s.(st_freshstate)
        s.(st_scldecls)
        (AssocMap.set r (i, VArray sz ln) s.(st_arrdecls))
-       s.(st_datapath)
-       s.(st_controllogic)).
+       s.(st_datapath)).
 Proof. Admitted.
 
 Definition declare_arr (i : option io) (r : reg) (sz : nat) (ln : nat) : mon unit :=
@@ -188,112 +187,9 @@ Definition declare_arr (i : option io) (r : reg) (sz : nat) (ln : nat) : mon uni
                 s.(st_freshstate)
                 s.(st_scldecls)
                 (AssocMap.set r (i, VArray sz ln) s.(st_arrdecls))
-                s.(st_datapath)
-                s.(st_controllogic))
+                s.(st_datapath))
               (declare_arr_state_incr i s r sz ln).
 
-Lemma add_instr_state_incr :
-  forall s preg p n n' st,
-    (st_controllogic s)!n = None ->
-    st_incr s
-    (mkstate
-       s.(st_st)
-       s.(st_freshreg)
-       (st_freshstate s)
-       s.(st_scldecls)
-       s.(st_arrdecls)
-       (AssocMap.set n st s.(st_datapath))
-       (AssocMap.set n (state_goto preg p s.(st_st) n') s.(st_controllogic))).
-Proof.
-  constructor; intros;
-    try (simpl; destruct (peq n n0); subst);
-    auto with htlh.
-Qed.
-
-Definition add_instr (preg: reg) (p: option pred_op) (n : node) (n' : node) (st : stmnt) : mon unit :=
-  fun s =>
-    match check_empty_node_controllogic s n with
-    | left TRANS =>
-      OK tt (mkstate
-               s.(st_st)
-               s.(st_freshreg)
-               (st_freshstate s)
-               s.(st_scldecls)
-               s.(st_arrdecls)
-               (AssocMap.set n st s.(st_datapath))
-               (AssocMap.set n (state_goto preg p s.(st_st) n') s.(st_controllogic)))
-         (add_instr_state_incr s preg p n n' st TRANS)
-    | _ => Error (Errors.msg "HTL.add_instr")
-    end.
-
-Lemma add_instr_skip_state_incr :
-  forall s n st,
-    (st_controllogic s)!n = None ->
-    st_incr s
-    (mkstate
-       s.(st_st)
-       s.(st_freshreg)
-       (st_freshstate s)
-       s.(st_scldecls)
-       s.(st_arrdecls)
-       (AssocMap.set n st s.(st_datapath))
-       (AssocMap.set n Vskip s.(st_controllogic))).
-Proof.
-  constructor; intros;
-    try (simpl; destruct (peq n n0); subst);
-    auto with htlh.
-Qed.
-
-Definition add_instr_skip (n : node) (st : stmnt) : mon unit :=
-  fun s =>
-    match check_empty_node_controllogic s n with
-    | left TRANS =>
-      OK tt (mkstate
-               s.(st_st)
-               s.(st_freshreg)
-               (st_freshstate s)
-               s.(st_scldecls)
-               s.(st_arrdecls)
-               (AssocMap.set n st s.(st_datapath))
-               (AssocMap.set n Vskip s.(st_controllogic)))
-         (add_instr_skip_state_incr s n st TRANS)
-    | _ => Error (Errors.msg "HTL.add_instr_skip")
-    end.
-
-Lemma add_node_skip_state_incr :
-  forall s n st,
-    (st_controllogic s)!n = None ->
-    st_incr s
-    (mkstate
-       s.(st_st)
-       s.(st_freshreg)
-       (st_freshstate s)
-       s.(st_scldecls)
-       s.(st_arrdecls)
-       (AssocMap.set n Vskip s.(st_datapath))
-       (AssocMap.set n st s.(st_controllogic))).
-Proof.
-  constructor; intros;
-    try (simpl; destruct (peq n n0); subst);
-    auto with htlh.
-Qed.
-
-Definition add_node_skip (n : node) (st : stmnt) : mon unit :=
-  fun s =>
-    match check_empty_node_controllogic s n with
-    | left TRANS =>
-      OK tt (mkstate
-               s.(st_st)
-               s.(st_freshreg)
-               (st_freshstate s)
-               s.(st_scldecls)
-               s.(st_arrdecls)
-               (AssocMap.set n Vskip s.(st_datapath))
-               (AssocMap.set n st s.(st_controllogic)))
-         (add_node_skip_state_incr s n st TRANS)
-    | _ => Error (Errors.msg "HTL.add_node_skip")
-    end.
-
 Definition nonblock (dst : reg) (e : expr) := Vnonblock (Vvar dst) e.
 Definition block (dst : reg) (e : expr) := Vblock (Vvar dst) e.
 
@@ -306,68 +202,57 @@ Definition boplit (op : binop) (r : reg) (l : Integers.int) : expr :=
 Definition boplitz (op: binop) (r: reg) (l: Z) : expr :=
   Vbinop op (Vvar r) (Vlit (ZToValue l)).
 
-Definition translate_comparison (c : Integers.comparison) (args : list reg)
-  : mon expr :=
+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 (Errors.msg
-                 "Htlgen: comparison instruction not implemented: other")
+  | Integers.Ceq, r1::r2::nil => Errors.OK (bop Veq r1 r2)
+  | Integers.Cne, r1::r2::nil => Errors.OK (bop Vne r1 r2)
+  | Integers.Clt, r1::r2::nil => Errors.OK (bop Vlt r1 r2)
+  | Integers.Cgt, r1::r2::nil => Errors.OK (bop Vgt r1 r2)
+  | Integers.Cle, r1::r2::nil => Errors.OK (bop Vle r1 r2)
+  | Integers.Cge, r1::r2::nil => Errors.OK (bop Vge r1 r2)
+  | _, _ => Errors.Error (Errors.msg "Htlgen: comparison instruction not implemented: other")
   end.
 
-Definition translate_comparison_imm (c : Integers.comparison) (args : list reg)
-           (i: Integers.int) : mon expr :=
+Definition translate_comparison_imm (c : Integers.comparison) (args : list reg) (i: Integers.int)
+  : Errors.res expr :=
   match c, args with
-  | Integers.Ceq, r1::nil => ret (boplit Veq r1 i)
-  | Integers.Cne, r1::nil => ret (boplit Vne r1 i)
-  | Integers.Clt, r1::nil => ret (boplit Vlt r1 i)
-  | Integers.Cgt, r1::nil => ret (boplit Vgt r1 i)
-  | Integers.Cle, r1::nil => ret (boplit Vle r1 i)
-  | Integers.Cge, r1::nil => ret (boplit Vge r1 i)
-  | _, _ => error (Errors.msg
-                 "Htlgen: comparison_imm instruction not implemented: other")
+  | 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)
+  | _, _ => Errors.Error (Errors.msg "Htlgen: comparison_imm instruction not implemented: other")
   end.
 
-Definition translate_comparisonu (c : Integers.comparison) (args : list reg)
-  : mon expr :=
+Definition translate_comparisonu (c : Integers.comparison) (args : list reg) : Errors.res expr :=
   match c, args with
-  | Integers.Clt, r1::r2::nil => ret (bop Vltu r1 r2)
-  | Integers.Cgt, r1::r2::nil => ret (bop Vgtu r1 r2)
-  | Integers.Cle, r1::r2::nil => ret (bop Vleu r1 r2)
-  | Integers.Cge, r1::r2::nil => ret (bop Vgeu r1 r2)
-  | _, _ => error (Errors.msg
-                 "Htlgen: comparison instruction not implemented: other")
+  | 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 "Htlgen: comparison instruction not implemented: other")
   end.
 
-Definition translate_comparison_immu (c : Integers.comparison)
-           (args : list reg) (i: Integers.int) : mon expr :=
+Definition translate_comparison_immu (c : Integers.comparison) (args : list reg) (i: Integers.int)
+  : Errors.res expr :=
   match c, args with
-  | Integers.Clt, r1::nil => ret (boplit Vltu r1 i)
-  | Integers.Cgt, r1::nil => ret (boplit Vgtu r1 i)
-  | Integers.Cle, r1::nil => ret (boplit Vleu r1 i)
-  | Integers.Cge, r1::nil => ret (boplit Vgeu r1 i)
-  | _, _ => error (Errors.msg
-                 "Htlgen: comparison_imm instruction not implemented: other")
+  | 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 "Htlgen: comparison_imm instruction not implemented: other")
   end.
 
-Definition translate_condition (c : Op.condition) (args : list reg)
-  : mon expr :=
+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, _ =>
-    error (Errors.msg "Htlgen: condition instruction not implemented: Cmaskzero")
-  | Op.Cmasknotzero n, _ =>
-    error (Errors.msg
-         "Htlgen: condition instruction not implemented: Cmasknotzero")
-  | _, _ =>
-    error (Errors.msg "Htlgen: condition instruction not implemented: other")
+  | Op.Cmaskzero n, _ => Errors.Error (Errors.msg "Htlgen: condition instruction not implemented: Cmaskzero")
+  | Op.Cmasknotzero n, _ => Errors.Error (Errors.msg "Htlgen: condition instruction not implemented: Cmasknotzero")
+  | _, _ => Errors.Error (Errors.msg "Htlgen: condition instruction not implemented: other")
   end.
 
 Definition check_address_parameter_signed (p : Z) : bool :=
@@ -377,136 +262,100 @@ Definition check_address_parameter_signed (p : Z) : bool :=
 Definition check_address_parameter_unsigned (p : Z) : bool :=
   Z.leb p Integers.Ptrofs.max_unsigned.
 
-Lemma create_reg_state_incr:
-  forall s sz i,
-    st_incr s (mkstate
-         s.(st_st)
-         (Pos.succ (st_freshreg s))
-         (st_freshstate s)
-         (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls))
-         s.(st_arrdecls)
-         (st_datapath s)
-         (st_controllogic s)).
-Proof. constructor; simpl; auto with htlh. Qed.
-
-Definition create_reg (i : option io) (sz : nat) : mon reg :=
-  fun s => let r := s.(st_freshreg) in
-           OK r (mkstate
-                   s.(st_st)
-                   (Pos.succ r)
-                   (st_freshstate s)
-                   (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls))
-                   (st_arrdecls s)
-                   (st_datapath s)
-                   (st_controllogic s))
-              (create_reg_state_incr s sz i).
-
-Definition translate_eff_addressing (a: Op.addressing) (args: list reg)
-  : mon expr :=
+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 ret (boplitz Vadd r1 off)
-    else error (Errors.msg ("HTLPargen: translate_eff_addressing (Aindexed): address out of bounds"))
+    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 ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue offset)))
-    else error (Errors.msg "HTLPargen: translate_eff_addressing (Ascaled): address out of bounds")
+    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 ret (Vbinop Vadd (bop Vadd r1 r2) (Vlit (ZToValue offset)))
-    else error (Errors.msg "HTLPargen: translate_eff_addressing (Aindexed2): address out of bounds")
+    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 ret (Vbinop Vadd (Vvar r1) (Vbinop Vadd (boplitz Vmul r2 scale) (Vlit (ZToValue offset))))
-    else error (Errors.msg "HTLPargen: translate_eff_addressing (Aindexed2scaled): address out of bounds")
+    then Errors.OK (Vbinop Vadd (Vvar 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 ret (Vlit (ZToValue a))
-    else error (Errors.msg "HTLPargen: translate_eff_addressing (Ainstack): address out of bounds")
-  | _, _ => error (Errors.msg "HTLPargen: translate_eff_addressing unsuported addressing")
+    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.
 
-(*|
-Translate an instruction to a statement. FIX mulhs mulhu
-|*)
+#[local] Close Scope monad_scope.
+#[local] Open Scope error_monad_scope.
 
-Definition translate_instr (op : Op.operation) (args : list reg) : mon expr :=
+(** 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 => ret (Vvar r)
-  | Op.Ointconst n, _ => ret (Vlit (intToValue n))
-  | Op.Oneg, r::nil => ret (Vunop Vneg (Vvar r))
-  | Op.Osub, r1::r2::nil => ret (bop Vsub r1 r2)
-  | Op.Omul, r1::r2::nil => ret (bop Vmul r1 r2)
-  | Op.Omulimm n, r::nil => ret (boplit Vmul r n)
-  | Op.Omulhs, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: mulhs")
-  | Op.Omulhu, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: mulhu")
-  | Op.Odiv, r1::r2::nil => ret (bop Vdiv r1 r2)
-  | Op.Odivu, r1::r2::nil => ret (bop Vdivu r1 r2)
-  | Op.Omod, r1::r2::nil => ret (bop Vmod r1 r2)
-  | Op.Omodu, r1::r2::nil => ret (bop Vmodu r1 r2)
-  | Op.Oand, r1::r2::nil => ret (bop Vand r1 r2)
-  | Op.Oandimm n, r::nil => ret (boplit Vand r n)
-  | Op.Oor, r1::r2::nil => ret (bop Vor r1 r2)
-  | Op.Oorimm n, r::nil => ret (boplit Vor r n)
-  | Op.Oxor, r1::r2::nil => ret (bop Vxor r1 r2)
-  | Op.Oxorimm n, r::nil => ret (boplit Vxor r n)
-  | Op.Onot, r::nil => ret (Vunop Vnot (Vvar r))
-  | Op.Oshl, r1::r2::nil => ret (bop Vshl r1 r2)
-  | Op.Oshlimm n, r::nil => ret (boplit Vshl r n)
-  | Op.Oshr, r1::r2::nil => ret (bop Vshr r1 r2)
-  | Op.Oshrimm n, r::nil => ret (boplit Vshr r n)
+  | Op.Omove, r::nil => Errors.OK (Vvar r)
+  | Op.Ointconst n, _ => Errors.OK (Vlit (intToValue n))
+  | Op.Oneg, r::nil => Errors.OK (Vunop Vneg (Vvar 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 "Htlgen: Instruction not implemented: mulhs")
+  | Op.Omulhu, r1::r2::nil => Errors.Error (Errors.msg "Htlgen: 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 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 =>
-    ret (Vternary (Vbinop Vlt (Vvar r) (Vlit (ZToValue 0)))
+    Errors.OK (Vternary (Vbinop Vlt (Vvar r) (Vlit (ZToValue 0)))
                   (Vunop Vneg (Vbinop Vshru (Vunop Vneg (Vvar r)) (Vlit n)))
                   (Vbinop Vshru (Vvar r) (Vlit n)))
-  | Op.Oshru, r1::r2::nil => ret (bop Vshru r1 r2)
-  | Op.Oshruimm n, r::nil => ret (boplit Vshru r n)
-  | Op.Ororimm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Ororimm")
-  (*ret (Vbinop Vor (boplit Vshru r (Integers.Int.modu n (Integers.Int.repr 32)))
+  | 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 "Htlgen: 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 => ret (Vbinop Vor (boplit Vshl r n) (boplit Vshr r (Integers.Int.sub (Integers.Int.repr 32) n)))
+  | 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;
-    ret (Vternary tc (Vvar r1) (Vvar r2))
+    Errors.OK (Vternary tc (Vvar r1) (Vvar r2))
   | Op.Olea a, _ => translate_eff_addressing a args
-  | _, _ => error (Errors.msg "Htlgen: Instruction not implemented: other")
+  | _, _ => Errors.Error (Errors.msg "Htlgen: Instruction not implemented: other")
   end.
 
-Lemma add_branch_instr_state_incr:
-  forall s preg p e n n1 n2,
-    (st_controllogic s) ! n = None ->
-    st_incr s (mkstate
-                 s.(st_st)
-                (st_freshreg s)
-                (st_freshstate s)
-                s.(st_scldecls)
-                s.(st_arrdecls)
-                (AssocMap.set n Vskip (st_datapath s))
-                (AssocMap.set n (state_cond preg p s.(st_st) e n1 n2) (st_controllogic s))).
-Proof.
-  intros. apply state_incr_intro; simpl;
-            try (intros; destruct (peq n0 n); subst);
-            auto with htlh.
-Qed.
-
-Definition add_branch_instr preg p (e: expr) (n n1 n2: node) : mon unit :=
-  fun s =>
-    match check_empty_node_controllogic s n with
-    | left NTRANS =>
-      OK tt (mkstate
-               s.(st_st)
-                (st_freshreg s)
-                (st_freshstate s)
-                s.(st_scldecls)
-                s.(st_arrdecls)
-                (AssocMap.set n Vskip (st_datapath s))
-                (AssocMap.set n (state_cond preg p s.(st_st) e n1 n2) (st_controllogic s)))
-         (add_branch_instr_state_incr s preg p e n n1 n2 NTRANS)
-    | _ => Error (Errors.msg "Htlgen: add_branch_instr")
-    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
@@ -516,12 +365,156 @@ Fixpoint enumerate (i : nat) (ns : list node) {struct ns} : list (nat * node) :=
 
 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)))
+                    (i, n) => (Vlit (natToValue i), Vnonblock (Vvar st) (Vlit (posToValue n)))
                   end)
            (enumerate 0 ns).
 
-Definition stack_correct (sz : Z) : bool :=
-  (0 <=? sz) && (sz <? Integers.Ptrofs.modulus) && (Z.modulo sz 4 =? 0).
+Definition translate_cfi (fin rtrn state preg: reg) p (cfi: cf_instr)
+  : Errors.res stmnt :=
+  match cfi with
+  | RBgoto n' =>
+    Errors.OK (state_goto preg p state n')
+  | RBcond c args n1 n2 =>
+    do e <- translate_condition c args;
+    Errors.OK (state_cond preg p state e n1 n2)
+  | RBreturn r =>
+    match r with
+    | Some r' =>
+      Errors.OK (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r')))
+    | None =>
+      Errors.OK (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vlit (ZToValue 0%Z))))
+    end
+  | RBjumptable r tbl =>
+    Errors.OK (Vcase (Vvar r) (list_to_stmnt (tbl_to_case_expr state 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 dfltp {A} (p: option (@Predicate.pred_op A)) := Option.default Ptrue p.
+
+Definition transf_instr (fin rtrn stack state preg: reg) 
+           (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 preg (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 stack;
+    let stmnt := translate_predicate Vblock preg (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 stack;
+    let stmnt := translate_predicate Vblock preg (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 preg (npred p') (pred_expr preg (Plit (true, p))) cond' in
+    Errors.OK (curr_p, Vseq d stmnt)
+  | RBexit p cf => 
+    do d_stmnt <- translate_cfi fin rtrn state preg (npred p) cf;
+    Errors.OK (Pand curr_p (negate (dfltp p)), Vseq d d_stmnt)
+  end.
+
+Definition fold_leftE {A B} (f: A -> B -> Errors.res A) (l: list B) (el: A): Errors.res A :=
+  fold_left (fun a b => do a' <- a; f a' b) l (Errors.OK el).
+
+Definition transf_chained_block (fin rtrn stack state preg: reg)
+           (dc: @pred_op positive * stmnt)
+           (block: list instr)
+           : Errors.res (pred_op * stmnt) :=
+  fold_leftE (transf_instr fin rtrn stack state preg) block dc.
+
+Definition transf_parallel_block (fin rtrn stack state preg: reg)
+           (dc: @pred_op positive * stmnt)
+           (block: list (list instr))
+           : Errors.res (pred_op * stmnt) :=
+  fold_leftE (transf_chained_block fin rtrn stack state preg) block dc.
+
+Definition transf_parallel_full_block (fin rtrn stack state preg: reg)
+           (dc: node * @pred_op positive * datapath)
+           (block: list (list instr))
+           : Errors.res (node * pred_op * datapath) :=
+  let '(n, curr_p, dt) := dc in
+  match AssocMap.get n dt with
+  | None =>
+    do ctrl_init_stmnt <-
+          translate_cfi fin rtrn state preg (Some curr_p) (RBgoto (n - 1)%positive);
+    do dc' <- transf_parallel_block fin rtrn stack state preg (curr_p, ctrl_init_stmnt) block;
+    let '(curr_p', dt_stmnt) := dc' in
+    Errors.OK ((n - 1)%positive, curr_p', AssocMap.set n dt_stmnt dt)
+  | _ => Errors.Error (msg "HtlPargen.transf_parallel_full_block: block not empty")
+  end.
+
+Definition transf_seq_block (fin rtrn stack state preg: reg)
+           (d: datapath) (n: node)
+           (block: list (list (list instr)))
+           : Errors.res datapath :=
+  do res <- fold_leftE
+    (transf_parallel_full_block fin rtrn stack state preg) block (n, Ptrue, d);
+  let '(_, _, d') := res in
+  Errors.OK d'.
+
+#[local] Close Scope error_monad_scope.
+#[local] Open Scope monad_scope.
+
+Program Definition transf_seq_blockM (fin rtrn stack preg: reg) (ni: node * ParBB.t): mon unit :=
+  fun st =>
+    let (n, i) := ni in
+    match transf_seq_block fin rtrn stack st.(st_st) preg st.(st_datapath) n i with
+    | Errors.OK d => 
+      OK tt (mkstate st.(st_st)
+             st.(st_freshreg)
+             st.(st_freshstate)
+             st.(st_scldecls)
+             st.(st_arrdecls)
+             d) _
+    | Errors.Error m => Error m
+    end.
+Next Obligation.
+admit.
+Admitted.
+
+Definition declare_regs (i: instr): mon unit :=
+  match i with
+  | RBop _ _ _ d => declare_reg None d 32
+  | RBload _ _ _ _ d => declare_reg None d 32
+  | _ => ret tt
+  end.
+
+Definition declare_all_regs (ni: node * ParBB.t): mon unit :=
+  let (n, i) := ni in
+  ParBB.foldl _ (fun (st_f: mon unit) i => do _tt <- st_f; declare_regs i) i (ret tt).
+
+Lemma create_reg_state_incr:
+  forall s sz i,
+    st_incr s (mkstate
+         s.(st_st)
+         (Pos.succ (st_freshreg s))
+         (st_freshstate s)
+         (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls))
+         s.(st_arrdecls)
+         (st_datapath s)).
+Proof. constructor; simpl; auto with htlh. Qed.
+
+Definition create_reg (i : option io) (sz : nat) : mon reg :=
+  fun s => let r := s.(st_freshreg) in
+           OK r (mkstate
+                   s.(st_st)
+                   (Pos.succ r)
+                   (st_freshstate s)
+                   (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls))
+                   (st_arrdecls s)
+                   (st_datapath s))
+              (create_reg_state_incr s sz i).
 
 Lemma create_arr_state_incr:
   forall s sz ln i,
@@ -531,8 +524,7 @@ Lemma create_arr_state_incr:
          (st_freshstate s)
          s.(st_scldecls)
          (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls))
-         (st_datapath s)
-         (st_controllogic s)).
+         (st_datapath s)).
 Proof. constructor; simpl; auto with htlh. Qed.
 
 Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) :=
@@ -543,17 +535,19 @@ Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) :=
                    (st_freshstate s)
                    s.(st_scldecls)
                    (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls))
-                   (st_datapath s)
-                   (st_controllogic s))
+                   (st_datapath s))
               (create_arr_state_incr s sz ln i).
 
+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.
+  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.
@@ -561,9 +555,8 @@ Proof.
   rewrite PTree.gempty. congruence.
   (* inductive case *)
   intros. rewrite PTree.gsspec in H2. destruct (peq pc k).
-  inv H2. unfold Ple, Plt in *. lia.
-  apply Ple_trans with a. auto.
-  unfold Ple, Plt in *. lia.
+  inv H2. unfold Ple; lia.
+  apply Ple_trans with a. auto. unfold Ple; lia.
 Qed.
 
 Lemma max_pc_wf :
@@ -577,282 +570,7 @@ Proof.
   simplify. transitivity (Z.pos (max_pc_map m)); eauto.
 Qed.
 
-Definition poslength {A : Type} (l : list A) : positive :=
-  match Zlength l with
-  | Z.pos p => p
-  | _ => 1
-  end.
-
-Fixpoint penumerate {A : Type} (p : positive) (l : list A) {struct l}
-  : list (positive * A) :=
-  match l with
-  | x :: xs => (p, x) :: penumerate (Pos.pred p) xs
-  | nil => nil
-  end.
-
-Fixpoint prange {A: Type} (p1 p2: positive) (l: list A) {struct l} :=
-  match l with
-  | x :: xs => (p1, p2, x) :: prange p2 (Pos.pred p2) xs
-  | nil => nil
-  end.
-
-Lemma add_data_instr_state_incr :
-  forall s n st,
-    st_incr s
-    (mkstate
-       s.(st_st)
-       s.(st_freshreg)
-       (st_freshstate s)
-       s.(st_scldecls)
-       s.(st_arrdecls)
-       (AssocMap.set n (Vseq (AssocMapExt.get_default
-                            _ Vskip n s.(st_datapath)) st) s.(st_datapath))
-       s.(st_controllogic)).
-Proof.
-  constructor; intros;
-    try (simpl; destruct (peq n n0); subst);
-    auto with htlh.
-Qed.
-
-Definition add_data_instr (n : node) (st : stmnt) : mon unit :=
-  fun s =>
-    OK tt (mkstate
-         s.(st_st)
-         s.(st_freshreg)
-         (st_freshstate s)
-         s.(st_scldecls)
-         s.(st_arrdecls)
-         (AssocMap.set n (Vseq (AssocMapExt.get_default _ Vskip n s.(st_datapath)) st) s.(st_datapath))
-         s.(st_controllogic))
-       (add_data_instr_state_incr s n st).
-
-Lemma add_control_instr_state_incr :
-  forall s n st,
-  (st_controllogic s) ! n = None ->
-    st_incr s
-    (mkstate
-       s.(st_st)
-       s.(st_freshreg)
-       (st_freshstate s)
-       s.(st_scldecls)
-       s.(st_arrdecls)
-       s.(st_datapath)
-       (AssocMap.set n st s.(st_controllogic))).
-Proof.
-  constructor; intros;
-    try (simpl; destruct (peq n n0); subst);
-    auto with htlh.
-Qed.
-
-Definition add_control_instr (n : node) (st : stmnt) : mon unit :=
-  fun s =>
-    match check_empty_node_controllogic s n with
-    | left CTRL =>
-      OK tt (mkstate
-           s.(st_st)
-           s.(st_freshreg)
-           (st_freshstate s)
-           s.(st_scldecls)
-           s.(st_arrdecls)
-           s.(st_datapath)
-           (AssocMap.set n st s.(st_controllogic)))
-         (add_control_instr_state_incr s n st CTRL)
-    | _ =>
-      Error (Errors.msg "HTLPargen.add_control_instr: control logic is not empty")
-    end.
-
-Definition add_control_instr_force_state_incr :
-  forall s n st,
-    st_incr s
-    (mkstate
-       s.(st_st)
-       s.(st_freshreg)
-       (st_freshstate s)
-       s.(st_scldecls)
-       s.(st_arrdecls)
-       s.(st_datapath)
-       (AssocMap.set n st s.(st_controllogic))).
-Admitted.
-
-Definition update_control_instr (n : node) (st : stmnt) : mon unit :=
-  fun s =>
-    match s.(st_controllogic) ! n with
-    | Some st' =>
-      OK tt (mkstate
-           s.(st_st)
-           s.(st_freshreg)
-           (st_freshstate s)
-           s.(st_scldecls)
-           s.(st_arrdecls)
-           s.(st_datapath)
-           (AssocMap.set n (Vseq st' st) s.(st_controllogic)))
-         (add_control_instr_force_state_incr s n (Vseq st' st))
-    | None =>
-      OK tt (mkstate
-           s.(st_st)
-           s.(st_freshreg)
-           (st_freshstate s)
-           s.(st_scldecls)
-           s.(st_arrdecls)
-           s.(st_datapath)
-           (AssocMap.set n st s.(st_controllogic)))
-         (add_control_instr_force_state_incr s n st)
-    end.
-
-Definition add_control_instr_force (n : node) (st : stmnt) : mon unit :=
-  fun s =>
-    OK tt (mkstate
-      s.(st_st)
-      s.(st_freshreg)
-      (st_freshstate s)
-      s.(st_scldecls)
-      s.(st_arrdecls)
-      s.(st_datapath)
-      (AssocMap.set n st s.(st_controllogic)))
-   (add_control_instr_force_state_incr s n st).
-
-Definition add_control_instr_try (n : node) (st : stmnt) : mon unit :=
-  fun s =>
-    match check_empty_node_controllogic s n with
-    | left CTRL =>
-      OK tt (mkstate
-           s.(st_st)
-           s.(st_freshreg)
-           (st_freshstate s)
-           s.(st_scldecls)
-           s.(st_arrdecls)
-           s.(st_datapath)
-           (AssocMap.set n st s.(st_controllogic)))
-         (add_control_instr_state_incr s n st CTRL)
-    | _ =>
-      OK tt s (st_refl s)
-    end.
-
-Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing)
-           (args : list reg) (stack : reg) : mon 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 ret (Vvari stack (Vbinop Vdivu (boplitz Vadd r1 off) (Vlit (ZToValue 4))))
-    else error (Errors.msg "HTLgen: 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 ret (Vvari stack
-                    (Vbinop Vdivu
-                            (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale))
-                            (Vlit (ZToValue 4))))
-    else error (Errors.msg "HTLgen: 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 ret (Vvari stack (Vlit (ZToValue (a / 4))))
-    else error (Errors.msg "HTLgen: eff_addressing out of bounds stack offset")
-  | _, _, _ => error (Errors.msg "HTLgen: translate_arr_access unsuported addressing")
-  end.
-
-Lemma create_new_state_state_incr:
-  forall s p,
-  st_incr s
-    (mkstate
-       s.(st_st)
-       s.(st_freshreg)
-       (s.(st_freshstate) + p)%positive
-       s.(st_scldecls)
-       s.(st_arrdecls)
-       s.(st_datapath)
-       s.(st_controllogic)).
-Admitted.
-
-Definition create_new_state (p: node): mon node :=
-  fun s => OK s.(st_freshstate)
-              (mkstate
-                s.(st_st)
-                s.(st_freshreg)
-                (s.(st_freshstate) + p)%positive
-                s.(st_scldecls)
-                s.(st_arrdecls)
-                s.(st_datapath)
-                s.(st_controllogic))
-              (create_new_state_state_incr s p).
-
-Definition translate_cfi' (fin rtrn preg: reg) p (cfi: cf_instr)
-  : mon (stmnt * stmnt) :=
-  match cfi with
-  | RBgoto n' =>
-    do st <- get;
-    ret (Vskip, state_goto preg p st.(st_st) n')
-  | RBcond c args n1 n2 =>
-    do st <- get;
-    do e <- translate_condition c args;
-    ret (Vskip, state_cond preg p st.(st_st) e n1 n2)
-  | RBreturn r =>
-    match r with
-    | Some r' =>
-      ret ((Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r'))),
-           Vskip)
-    | None =>
-      ret ((Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vlit (ZToValue 0%Z)))),
-           Vskip)
-    end
-  | RBjumptable r tbl =>
-    do s <- get;
-    ret (Vskip, Vcase (Vvar r) (list_to_stmnt (tbl_to_case_expr s.(st_st) tbl)) (Some Vskip))
-  | RBcall sig ri rl r n =>
-    error (Errors.msg "HTLPargen: RPcall not supported.")
-  | RBtailcall sig ri lr =>
-    error (Errors.msg "HTLPargen: RPtailcall not supported.")
-  | RBbuiltin e lb b n =>
-    error (Errors.msg "HTLPargen: RPbuildin not supported.")
-  end.
-
-Definition translate_cfi (fin rtrn preg: reg) p (ni: node * cf_instr) : mon unit :=
-  let (n, cfi) := ni in
-  do (s, c) <- translate_cfi' fin rtrn preg p cfi;
-  do _ <- update_control_instr n c;
-  add_data_instr n s.
-
-Definition translate_inst a (fin rtrn preg stack : reg) (n : node) (i : instr) :=
-  match i with
-  | RBnop =>
-    do stmnt <- ret Vskip;
-    add_data_instr n stmnt
-  | RBop p op args dst =>
-    do instr <- translate_instr op args;
-    do _ <- declare_reg None dst 32;
-    add_data_instr n (translate_predicate a preg p (Vvar dst) instr)
-  | RBload p mem addr args dst =>
-    do src <- translate_arr_access mem addr args stack;
-    do _ <- declare_reg None dst 32;
-    add_data_instr n (translate_predicate a preg p (Vvar dst) src)
-  | RBstore p mem addr args src =>
-    do dst <- translate_arr_access mem addr args stack;
-    add_data_instr n (translate_predicate a preg p dst (Vvar src))
-  | RBsetpred _ c args p =>
-    do cond <- translate_condition c args;
-    do stmnt <- ret (a (pred_expr preg (Plit (true, p))) cond);
-    add_data_instr n stmnt
-  | RBexit p cf =>
-    translate_cfi fin rtrn preg p (n, cf)
-  end.
-
-Definition translate_inst_list (fin rtrn preg stack: reg) (ni : node * node * list (list instr)) :=
-  match ni with
-  | (n, p, li) =>
-      do st <- get;
-      do _ <- add_control_instr n (state_goto preg None st.(st_st) p);
-      collectlist (fun l => translate_inst Vblock fin rtrn preg stack n l) (concat li)
-  end.
-
-Definition transf_bblock (fin rtrn preg stack: reg) (ni : node * ParBB.t)
-  : mon unit :=
-  let (n, bb) := ni in
-  do nstate <- create_new_state ((poslength bb))%positive;
-  do _ <- add_control_instr nstate Vskip;
-  collectlist (translate_inst_list fin rtrn preg stack)
-                      (prange n (nstate + poslength bb - 1)%positive
-                                  bb).
-
-(*Definition decide_order a b c d e f g : {module_ordering a b c d e f g} + {True}.
+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 _
@@ -861,67 +579,50 @@ Definition transf_bblock (fin rtrn preg stack: reg) (ni : node * ParBB.t)
   simplify; repeat match goal with
                    | H: context[(_ <? _)%positive] |- _ => apply Pos.ltb_lt in H
                    end; unfold module_ordering; auto.
-Defined.*)
-
-Lemma clk_greater :
-  forall ram clk r',
-    Some ram = Some r' -> (clk < ram_addr r')%positive.
-Proof. Admitted.
+Defined.
 
-Definition declare_ram (r: ram) : mon unit :=
-  do _ <- declare_reg None r.(ram_en) 1;
-  do _ <- declare_reg None r.(ram_u_en) 1;
-  do _ <- declare_reg None r.(ram_wr_en) 1;
-  do _ <- declare_reg None r.(ram_addr) 32;
-  do _ <- declare_reg None r.(ram_d_in) 32;
-  do _ <- declare_reg None r.(ram_d_out) 32;
-  do _ <- declare_arr None r.(ram_mem) 32 r.(ram_size);
-  ret tt.
-
-Definition transf_module (f: function) : mon HTL.module :=
+Definition transf_module (f: function) : mon DHTL.module.
+  refine (
   if stack_correct f.(fn_stacksize) then
     do fin <- create_reg (Some Voutput) 1;
     do rtrn <- create_reg (Some Voutput) 32;
-    do preg <- create_reg None 128;
+    do preg <- create_reg None 32;
     do (stack, stack_len) <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4));
-    do _ <- collectlist (transf_bblock fin rtrn preg stack)
-                        (Maps.PTree.elements f.(fn_code));
-    do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32)
-                        f.(fn_params);
+    do _stmnt <- collectlist (transf_seq_blockM fin rtrn stack preg) (Maps.PTree.elements f.(GiblePar.fn_code));
+    do _stmnt' <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(GiblePar.fn_params);
+    do _stmnt'' <- collectlist declare_all_regs (Maps.PTree.elements f.(GiblePar.fn_code));
     do start <- create_reg (Some Vinput) 1;
     do rst <- create_reg (Some Vinput) 1;
     do clk <- create_reg (Some Vinput) 1;
-    do r_en <- create_reg None 1;
-    do r_u_en <- create_reg None 1;
-    do r_addr <- create_reg None 32;
-    do r_wr_en <- create_reg None 1;
-    do r_d_in <- create_reg None 32;
-    do r_d_out <- create_reg None 32;
     do current_state <- get;
-    match zle (Z.pos (max_pc_map current_state.(st_datapath)))
-              Integers.Int.max_unsigned,
-      zle (Z.pos (max_pc_map current_state.(st_controllogic)))
-          Integers.Int.max_unsigned,
-      max_list_dec (fn_params f) (st_st current_state)
+    match zle (Z.pos (max_pc_map current_state.(st_datapath))) Integers.Int.max_unsigned,
+          decide_order (st_st current_state) fin rtrn stack start rst clk,
+          max_list_dec (GiblePar.fn_params f) (st_st current_state)
     with
-    | left LEDATA, left LECTRL, left WFPARAMS =>
-        ret (HTL.mkmodule
-        f.(fn_params)
-        current_state.(st_datapath)
-        current_state.(st_controllogic)
-        f.(fn_entrypoint)
-        current_state.(st_st)
-        fin
-        rtrn
-        start
-        rst
-        clk
-        current_state.(st_scldecls)
-        current_state.(st_arrdecls)
-        (mk_ram stack_len stack r_en r_u_en r_addr r_wr_en r_d_in r_d_out))
-    | _, _, _=> error (Errors.msg "More than 2^32 states.")
+    | left LEDATA, left MORD, left WFPARAMS =>
+        ret (DHTL.mkmodule
+           f.(GiblePar.fn_params)
+           current_state.(st_datapath)
+           f.(fn_entrypoint)
+           current_state.(st_st)
+           stack
+           stack_len
+           fin
+           rtrn
+           start
+           rst
+           clk
+           current_state.(st_scldecls)
+           current_state.(st_arrdecls)
+           None
+           (max_pc_wf _ LEDATA)
+           MORD
+           _
+           WFPARAMS)
+    | _, _, _ => error (Errors.msg "More than 2^32 states.")
     end
-  else error (Errors.msg "Stack size misalignment.").
+  else error (Errors.msg "Stack size misalignment.")); discriminate.
+Defined.
 
 Definition max_state (f: function) : state :=
   let st := Pos.succ (max_reg_function f) in
@@ -930,10 +631,9 @@ Definition max_state (f: function) : state :=
           (Pos.succ (max_pc_function f))
           (AssocMap.set st (None, VScalar 32) (st_scldecls (init_state st)))
           (st_arrdecls (init_state st))
-          (st_datapath (init_state st))
-          (st_controllogic (init_state st)).
+          (st_datapath (init_state st)).
 
-Definition transl_module (f : function) : Errors.res HTL.module :=
+Definition transl_module (f : function) : Errors.res DHTL.module :=
   run_mon (max_state f) (transf_module f).
 
 Definition transl_fundef := transf_partial_fundef transl_module.
@@ -949,7 +649,7 @@ Definition main_is_internal (p : GiblePar.program) : bool :=
   | _ => false
   end.
 
-Definition transl_program (p : GiblePar.program) : Errors.res HTL.program :=
+Definition transl_program (p : GiblePar.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.").