Add HTLBlockgen and more scheduling

9 files changed, 1041 insertions, 45 deletions

diff --git a/.ocamlformat b/.ocamlformat
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/.ocamlformat
diff --git a/Makefile b/Makefile
index 84908b8..ee111eb 100644
--- a/Makefile
+++ b/Makefile
@@ -38,6 +38,7 @@ lib/COMPCERTSTAMP:
 
 install:
 	install -d $(PREFIX)/bin
+	sed -i'' -e 's/arch=verilog/arch=x86/' _build/default/driver/compcert.ini
 	install -C _build/default/driver/compcert.ini $(PREFIX)/bin/.
 	install -C _build/default/driver/VericertDriver.exe $(PREFIX)/bin/vericert
 
diff --git a/example/explanation.org b/example/explanation.org
new file mode 100644
index 0000000..793c890
--- /dev/null
+++ b/example/explanation.org
@@ -0,0 +1,81 @@
+#+title: Interesting edge case in Simulation and Synthesis Mismatch
+
+I have always known about situations where the simulation might not match the synthesised result, for example when blocking assignment is used in one always block and is read from another.  However, the following mismatch is slightly surprising to me because I feel like simulators should be giving the same result as synthesis tools, as it seems to be quite common.  Otherwise, it also seems fair that the synthesis tool should implement what the simulator is showing, as it is strange to get such different results.
+
+I tested the following with the Quartus 20.1 and Yosys 0.9+2406 synthesis tool (which both gave the same result) and the icarus verilog, verilator and ModelSim simulators which also agreed with each other.
+
+Assuming we want to implement the following design.  My expectation would be that it just basically assigns ~a~ to ~x~ whenever ~a~ changes.
+
+#+begin_src verilog
+module top(a, x);
+   reg [3:0] tmp;
+   input [3:0] a;
+   output reg [3:0] x;
+
+   always @* begin
+      x = tmp;
+      tmp = a;
+   end
+endmodule // top
+#+end_src
+
+This seems to be correct when looking at the synthesised design printed by Yosys.
+
+#+begin_src verilog
+/* Generated by Yosys 0.9+2406 (git sha1 000fd08198, clang++ 7.1.0 -fPIC -Os) */
+module top_synth(a, x);
+  input [3:0] a;
+  wire [3:0] tmp;
+  output [3:0] x;
+  assign tmp = a;
+  assign x = a;
+endmodule
+#+end_src
+
+However, when simulating it with the following testbench, it instead acts like a shift register.
+
+#+begin_src verilog
+module main;
+   reg [3:0] a;
+   wire [3:0] x, x_synth;
+
+   top top(a, x);
+   top_synth top_synth(a, x_synth);
+
+   initial begin
+      a = 0;
+      #10 a = 1;
+      #10 $display("x: %d\nx_synth: %d", x, x_synth);
+      $finish;
+   end
+endmodule
+#+end_src
+
+The test bench above prints
+
+#+begin_src text
+x:  0
+x_synth:  1
+#+end_src
+
+showing that the synthesised design does not match the simulated design.
+
+Is the test bench that I wrote slightly broken?  Or is this expected to be this different.  In the latter case, how come simulators don't implement the correct behaviour?  This could be done by recursing and reevaluating the always block when an element in the sensitivity list changed, even if that was in the same always block.
+
+Even in simulation I would expect these two snippets to act the same
+
+#+begin_src verilog
+always @* begin
+   x = tmp;
+   tmp = a;
+end
+#+end_src
+
+#+begin_src verilog
+always @* begin
+   tmp = a;
+   x = tmp;
+end
+#+end_src
+
+Because ~a~ and ~tmp~ are both in the sensitivity list, meaning in the first code snippet, it should reevaluate the always block and update the ~x~ register with the correct value which is ~a~.
diff --git a/example/interesting.v b/example/interesting.v
new file mode 100644
index 0000000..c76f92a
--- /dev/null
+++ b/example/interesting.v
@@ -0,0 +1,36 @@
+module top(a, x);
+   reg [3:0] tmp;
+   input [3:0] a;
+   output reg [3:0] x;
+
+   always @* begin
+      x = tmp;
+      tmp = a;
+   end
+endmodule // top
+
+`ifndef SYNTHESIS
+/* Generated by Yosys 0.9+2406 (git sha1 000fd08198, clang++ 7.1.0 -fPIC -Os) */
+module top_synth(a, x);
+  input [3:0] a;
+  wire [3:0] tmp;
+  output [3:0] x;
+  assign tmp = a;
+  assign x = a;
+endmodule
+
+module main;
+   reg [3:0] a;
+   wire [3:0] x, x_synth;
+
+   top top(a, x);
+   top_synth top_synth(a, x_synth);
+
+   initial begin
+      a = 0;
+      #10 a = 1;
+      #10 $display("x: %d\nx_synth: %d", x, x_synth);
+      $finish;
+   end
+endmodule
+`endif
diff --git a/src/hls/HTLBlockgen.v b/src/hls/HTLBlockgen.v
new file mode 100644
index 0000000..12c63ce
--- /dev/null
+++ b/src/hls/HTLBlockgen.v
@@ -0,0 +1,654 @@
+(* 
+ * Vericert: Verified high-level synthesis.
+ * Copyright (C) 2020 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/>.
+ *)
+
+From compcert Require Import Maps.
+From compcert Require Errors Globalenvs Integers.
+From compcert Require Import AST RTLBlock.
+From vericert Require Import Verilog HTL Vericertlib AssocMap ValueInt Statemonad.
+
+Hint Resolve AssocMap.gempty : htlh.
+Hint Resolve AssocMap.gso : htlh.
+Hint Resolve AssocMap.gss : htlh.
+Hint Resolve Ple_refl : htlh.
+Hint Resolve Ple_succ : htlh.
+
+Record state: Type := mkstate {
+  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 :=
+  mkstate st
+          1%positive
+          1%positive
+          (AssocMap.empty (option io * scl_decl))
+          (AssocMap.empty (option io * arr_decl))
+          (AssocMap.empty stmnt)
+          (AssocMap.empty stmnt).
+
+Module HTLState <: State.
+
+  Definition st := state.
+
+  Inductive st_incr: state -> state -> Prop :=
+    state_incr_intro:
+      forall (s1 s2: state),
+        st_st s1 = st_st s2 ->
+        Ple s1.(st_freshreg) s2.(st_freshreg) ->
+        Ple s1.(st_freshstate) s2.(st_freshstate) ->
+        (forall n,
+            s1.(st_datapath)!n = None \/ s2.(st_datapath)!n = s1.(st_datapath)!n) ->
+        (forall n,
+            s1.(st_controllogic)!n = None
+            \/ s2.(st_controllogic)!n = s1.(st_controllogic)!n) ->
+        st_incr s1 s2.
+  Hint Constructors st_incr : htlh.
+
+  Definition st_prop := st_incr.
+  Hint Unfold st_prop : htlh.
+
+  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 H8 with n; intuition congruence.
+    - destruct H5 with n; destruct H9 with n; intuition congruence.
+  Qed.
+
+End HTLState.
+Export HTLState.
+
+Module HTLMonad := Statemonad(HTLState).
+Export HTLMonad.
+
+Module HTLMonadExtra := Monad.MonadExtra(HTLMonad).
+Import HTLMonadExtra.
+Export MonadNotation.
+
+Definition state_goto (st : reg) (n : node) : stmnt :=
+  Vnonblock (Vvar st) (Vlit (posToValue n)).
+
+Definition state_cond (st : reg) (c : expr) (n1 n2 : node) : stmnt :=
+  Vnonblock (Vvar st) (Vternary c (posToExpr n1) (posToExpr n2)).
+
+Definition check_empty_node_datapath:
+  forall (s: state) (n: node), { s.(st_datapath)!n = None } + { True }.
+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.
+
+Lemma add_instr_state_incr :
+  forall s n n' st,
+    (st_datapath s)!n = None ->
+    (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 s.(st_st) n') s.(st_controllogic))).
+Proof.
+  constructor; intros;
+    try (simpl; destruct (peq n n0); subst);
+    auto with htlh.
+Qed.
+
+Lemma declare_reg_state_incr :
+  forall i s r sz,
+    st_incr s
+    (mkstate
+       s.(st_st)
+       s.(st_freshreg)
+       s.(st_freshstate)
+       (AssocMap.set r (i, VScalar sz) s.(st_scldecls))
+       s.(st_arrdecls)
+       s.(st_datapath)
+       s.(st_controllogic)).
+Proof. auto with htlh. Qed.
+
+Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit :=
+  fun s => OK tt (mkstate
+                s.(st_st)
+                s.(st_freshreg)
+                s.(st_freshstate)
+                (AssocMap.set r (i, VScalar sz) s.(st_scldecls))
+                s.(st_arrdecls)
+                s.(st_datapath)
+                s.(st_controllogic))
+              (declare_reg_state_incr i s r sz).
+
+Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit :=
+  fun s =>
+    match check_empty_node_datapath s n, check_empty_node_controllogic s n with
+    | left STM, 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 s.(st_st) n') s.(st_controllogic)))
+         (add_instr_state_incr s n n' st STM TRANS)
+    | _, _ => Error (Errors.msg "HTL.add_instr")
+    end.
+
+Lemma add_instr_skip_state_incr :
+  forall s n st,
+    (st_datapath s)!n = None ->
+    (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_datapath s n, check_empty_node_controllogic s n with
+    | left STM, 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 STM TRANS)
+    | _, _ => Error (Errors.msg "HTL.add_instr")
+    end.
+
+Lemma add_node_skip_state_incr :
+  forall s n st,
+    (st_datapath s)!n = None ->
+    (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_datapath s n, check_empty_node_controllogic s n with
+    | left STM, 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 STM TRANS)
+    | _, _ => Error (Errors.msg "HTL.add_instr")
+    end.
+
+Definition nonblock (dst : reg) (e : expr) := Vnonblock (Vvar dst) e.
+Definition block (dst : reg) (e : expr) := Vblock (Vvar dst) e.
+
+Definition bop (op : binop) (r1 r2 : reg) : expr :=
+  Vbinop op (Vvar r1) (Vvar r2).
+
+Definition boplit (op : binop) (r : reg) (l : Integers.int) : expr :=
+  Vbinop op (Vvar r) (Vlit (intToValue l)).
+
+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 :=
+  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")
+  end.
+
+Definition translate_comparison_imm (c : Integers.comparison) (args : list reg) (i: Integers.int)
+  : mon 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")
+  end.
+
+Definition translate_comparisonu (c : Integers.comparison) (args : list reg) : mon 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")
+  end.
+
+Definition translate_comparison_immu (c : Integers.comparison) (args : list reg) (i: Integers.int)
+  : mon 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")
+  end.
+
+Definition translate_condition (c : Op.condition) (args : list reg) : mon 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")
+  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) : mon 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 "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 "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 "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 "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 "Veriloggen: translate_eff_addressing (Ainstack): address out of bounds")
+  | _, _ => error (Errors.msg "Veriloggen: translate_eff_addressing unsuported addressing")
+  end.
+
+(** Translate an instruction to a statement. FIX mulhs mulhu *)
+Definition translate_instr (op : Op.operation) (args : list reg) : mon 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.Oshrximm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Oshrximm")
+  (*ret (Vbinop Vdiv (Vvar r)
+    (Vbinop Vshl (Vlit (ZToValue 1))
+    (Vlit (intToValue 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)))
+                                        (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.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))
+  | Op.Olea a, _ => translate_eff_addressing a args
+  | _, _ => error (Errors.msg "Htlgen: Instruction not implemented: other")
+  end.
+
+Lemma add_branch_instr_state_incr:
+  forall s e n n1 n2,
+    (st_datapath s) ! n = None ->
+    (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 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 (e: expr) (n n1 n2: node) : mon unit :=
+  fun s =>
+    match check_empty_node_datapath s n, check_empty_node_controllogic s n with
+    | left NSTM, 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 s.(st_st) e n1 n2) (st_controllogic s)))
+         (add_branch_instr_state_incr s e n n1 n2 NSTM 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) : 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.
+
+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), Vnonblock (Vvar st) (Vlit (posToValue n)))
+                  end)
+           (enumerate 0 ns).
+
+Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit :=
+  match ni with
+    (n, i) =>
+    match i with
+    | Inop n' =>
+      if Z.leb (Z.pos n') Integers.Int.max_unsigned then
+        add_instr n n' Vskip
+      else error (Errors.msg "State is larger than 2^32.")
+    | Iop op args dst n' =>
+      if Z.leb (Z.pos n') Integers.Int.max_unsigned then
+        do instr <- translate_instr op args;
+        do _ <- declare_reg None dst 32;
+        add_instr n n' (nonblock dst instr)
+      else error (Errors.msg "State is larger than 2^32.")
+    | Iload mem addr args dst n' =>
+      if Z.leb (Z.pos n') Integers.Int.max_unsigned then
+        do src <- translate_arr_access mem addr args stack;
+        do _ <- declare_reg None dst 32;
+        add_instr n n' (nonblock dst src)
+      else error (Errors.msg "State is larger than 2^32.")
+    | Istore mem addr args src n' =>
+      if Z.leb (Z.pos n') Integers.Int.max_unsigned then
+        do dst <- translate_arr_access mem addr args stack;
+        add_instr n n' (Vnonblock dst (Vvar src)) (* TODO: Could juse use add_instr? reg exists. *)
+      else error (Errors.msg "State is larger than 2^32.")
+    | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.")
+    | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.")
+    | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.")
+    | Icond cond args n1 n2 =>
+      if Z.leb (Z.pos n1) Integers.Int.max_unsigned && Z.leb (Z.pos n2) Integers.Int.max_unsigned then
+        do e <- translate_condition cond args;
+        add_branch_instr e n n1 n2
+      else error (Errors.msg "State is larger than 2^32.")
+    | Ijumptable r tbl =>
+      (*do s <- get;
+      add_node_skip n (Vcase (Vvar r) (tbl_to_case_expr s.(st_st) tbl) (Some Vskip))*)
+      error (Errors.msg "Ijumptable: Case statement not supported.")
+    | Ireturn r =>
+      match r with
+      | Some r' =>
+        add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r')))
+      | None =>
+        add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vlit (ZToValue 0%Z))))
+      end
+    end
+  end.
+
+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).
+
+Lemma create_arr_state_incr:
+  forall s sz ln i,
+    st_incr s (mkstate
+         s.(st_st)
+         (Pos.succ (st_freshreg s))
+         (st_freshstate s)
+         s.(st_scldecls)
+         (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls))
+         (st_datapath s)
+         (st_controllogic s)).
+Proof. constructor; simpl; auto with htlh. Qed.
+
+Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) :=
+  fun s => let r := s.(st_freshreg) in
+           OK (r, ln) (mkstate
+                   s.(st_st)
+                   (Pos.succ r)
+                   (st_freshstate s)
+                   s.(st_scldecls)
+                   (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls))
+                   (st_datapath s)
+                   (st_controllogic 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. 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. xomega.
+  apply Ple_trans with a. auto. xomega.
+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 transf_module (f: function) : mon module :=
+  if stack_correct f.(fn_stacksize) then
+    do fin <- create_reg (Some Voutput) 1;
+    do rtrn <- create_reg (Some Voutput) 32;
+    do (stack, stack_len) <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4));
+    do _ <- collectlist (transf_instr fin rtrn stack) (Maps.PTree.elements f.(RTL.fn_code));
+    do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(RTL.fn_params);
+    do start <- create_reg (Some Vinput) 1;
+    do rst <- create_reg (Some Vinput) 1;
+    do clk <- create_reg (Some Vinput) 1;
+    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 with
+    | left LEDATA, left LECTRL =>
+        ret (mkmodule
+           f.(RTL.fn_params)
+           current_state.(st_datapath)
+           current_state.(st_controllogic)
+           f.(fn_entrypoint)
+           current_state.(st_st)
+           stack
+           stack_len
+           fin
+           rtrn
+           start
+           rst
+           clk
+           current_state.(st_scldecls)
+           current_state.(st_arrdecls)
+           (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA)))
+    | _, _ => error (Errors.msg "More than 2^32 states.")
+    end
+  else error (Errors.msg "Stack size misalignment.").
+
+Definition max_state (f: function) : state :=
+  let st := Pos.succ (max_reg_function f) in
+  mkstate st
+          (Pos.succ st)
+          (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)).
+
+Definition transl_module (f : function) : Errors.res module :=
+  run_mon (max_state f) (transf_module f).
+
+Definition transl_fundef := transf_partial_fundef transl_module.
+
+(* Definition transl_program (p : RTL.program) := transform_partial_program transl_fundef p. *)
+
+(*Definition transl_main_fundef f : Errors.res HTL.fundef :=
+  match f with
+  | Internal f => transl_fundef (Internal f)
+  | External f => Errors.Error (Errors.msg "Could not find internal main function")
+  end.
+
+(** Translation of a whole program. *)
+
+Definition transl_program (p: RTL.program) : Errors.res HTL.program :=
+  transform_partial_program2 (fun i f => if Pos.eqb p.(AST.prog_main) i
+                                         then transl_fundef f
+                                         else transl_main_fundef f)
+                             (fun i v => Errors.OK v) p.
+*)
+
+Definition main_is_internal (p : RTLBlock.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 : RTLBlock.program) : Errors.res HTL.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/Schedule.ml b/src/hls/Schedule.ml
index 2d9a7c2..7d2d2ea 100644
--- a/src/hls/Schedule.ml
+++ b/src/hls/Schedule.ml
@@ -42,91 +42,113 @@ let read_process command =
   Buffer.contents buffer
 
 let add_dep i tree deps curr =
-  match PTree.get curr tree with
-  | None -> deps
-  | Some ip -> (ip, i)::deps
+  match PTree.get curr tree with None -> deps | Some ip -> (ip, i) :: deps
 
 let accumulate_deps dfg curr =
-  let (i, tree, vals) = dfg in
+  let i, tree, vals = dfg in
   match curr with
-  | RBnop -> (i+1, tree, vals)
+  | RBnop -> (i + 1, tree, vals)
   | RBop (_, rs, dst) ->
-    (i+1,
-     PTree.set dst i tree,
-     List.append (List.fold_left (add_dep i tree) [] rs) vals)
-  | _ -> assert false
+      ( i + 1,
+        PTree.set dst i tree,
+        List.append (List.fold_left (add_dep i tree) [] rs) vals )
+  | RBload (mem, addr, rs, dst) ->
+      ( i + 1,
+        PTree.set dst i tree,
+        List.append (List.fold_left (add_dep i tree) [] rs) vals )
+  | RBstore (mem, addr, rs, dst) -> (i + 1, tree, vals)
 
 let assigned_vars vars = function
   | RBnop -> vars
-  | RBop (_, _, dst) -> dst::vars
-  | RBload (_, _, _, dst) -> dst::vars
+  | RBop (_, _, dst) -> dst :: vars
+  | RBload (_, _, _, dst) -> dst :: vars
   | RBstore (_, _, _, _) -> vars
 
 (* All the nodes in the DFG have to come after the source of the basic block, and should terminate
    before the sink of the basic block.  After that, there should be constraints for data
    dependencies between nodes. *)
 let gather_bb_constraints bb =
-  let (_, _, edges) = List.fold_left accumulate_deps (0, PTree.empty, []) bb.bb_body in
+  let _, _, edges =
+    List.fold_left accumulate_deps (0, PTree.empty, []) bb.bb_body
+  in
   match bb.bb_exit with
   | None -> assert false
-  | Some e ->
-  (List.length bb.bb_body, edges, successors_instr e)
+  | Some e -> (List.length bb.bb_body, edges, successors_instr e)
 
 let gen_bb_name s i = sprintf "bb%d%s" (P.to_int i) s
+
 let gen_bb_name_ssrc = gen_bb_name "ssrc"
+
 let gen_bb_name_ssnk = gen_bb_name "ssnk"
 
 let gen_var_name s c i = sprintf "v%d%s_%d" (P.to_int i) s c
+
 let gen_var_name_b = gen_var_name "b"
+
 let gen_var_name_e = gen_var_name "e"
 
 let print_lt0 = sprintf "%s - %s <= 0;\n"
 
-let print_bb_order i c =
-  print_lt0 (gen_bb_name_ssnk i) (gen_bb_name_ssrc c)
+let print_bb_order i c = print_lt0 (gen_bb_name_ssnk i) (gen_bb_name_ssrc c)
 
 let print_src_order i c =
-  print_lt0 (gen_bb_name_ssrc i) (gen_var_name_b c i) ^
-  print_lt0 (gen_var_name_e c i) (gen_bb_name_ssnk i) ^
-  sprintf "%s - %s = 1;\n" (gen_var_name_e c i) (gen_var_name_b c i)
+  print_lt0 (gen_bb_name_ssrc i) (gen_var_name_b c i)
+  ^ print_lt0 (gen_var_name_e c i) (gen_bb_name_ssnk i)
+  ^ sprintf "%s - %s = 1;\n" (gen_var_name_e c i) (gen_var_name_b c i)
 
 let print_src_type i c =
-  sprintf "int %s;\n" (gen_var_name_e c i) ^
-  sprintf "int %s;\n" (gen_var_name_b c i)
+  sprintf "int %s;\n" (gen_var_name_e c i)
+  ^ sprintf "int %s;\n" (gen_var_name_b c i)
 
 let print_data_dep_order c (i, j) =
   print_lt0 (gen_var_name_e i c) (gen_var_name_b j c)
 
 let rec gather_cfg_constraints (completed, (bvars, constraints, types)) c curr =
-  if List.exists (fun x -> P.eq x curr) completed then (completed, (bvars, constraints, types))
-  else match PTree.get curr c with
+  if List.exists (fun x -> P.eq x curr) completed then
+    (completed, (bvars, constraints, types))
+  else
+    match PTree.get curr c with
     | None -> assert false
     | Some (num_iters, edges, next) ->
-      let constraints' =
-        constraints ^
-        String.concat "" (List.map (print_bb_order curr) next) ^
-        String.concat "" (List.map (print_src_order curr) (List.init num_iters (fun x -> x))) ^
-        String.concat "" (List.map (print_data_dep_order curr) edges) in
-      let types' =
-        types ^
-        String.concat "" (List.map (print_src_type curr) (List.init num_iters (fun x -> x))) ^
-        sprintf "int %s;\n" (gen_bb_name_ssrc curr) ^
-        sprintf "int %s;\n" (gen_bb_name_ssnk curr) in
-      let bvars' =
-        List.append (List.map (fun x -> gen_var_name_b x curr)
-                       (List.init num_iters (fun x -> x))) bvars in
-      let next' = List.filter (fun x -> P.lt x curr) next in
-      List.fold_left (fun compl curr' -> gather_cfg_constraints compl c curr')
-        (curr::completed, (bvars', constraints', types')) next'
+        let constraints' =
+          constraints
+          ^ String.concat "" (List.map (print_bb_order curr) next)
+          ^ String.concat ""
+              (List.map (print_src_order curr)
+                 (List.init num_iters (fun x -> x)))
+          ^ String.concat "" (List.map (print_data_dep_order curr) edges)
+        in
+        let types' =
+          types
+          ^ String.concat ""
+              (List.map (print_src_type curr)
+                 (List.init num_iters (fun x -> x)))
+          ^ sprintf "int %s;\n" (gen_bb_name_ssrc curr)
+          ^ sprintf "int %s;\n" (gen_bb_name_ssnk curr)
+        in
+        let bvars' =
+          List.append
+            (List.map
+               (fun x -> gen_var_name_b x curr)
+               (List.init num_iters (fun x -> x)))
+            bvars
+        in
+        let next' = List.filter (fun x -> P.lt x curr) next in
+        List.fold_left
+          (fun compl curr' -> gather_cfg_constraints compl c curr')
+          (curr :: completed, (bvars', constraints', types'))
+          next'
 
 let rec intersperse s = function
   | [] -> []
-  | [a] -> [a]
-  | x::xs -> x::s::intersperse s xs
+  | [ a ] -> [ a ]
+  | x :: xs -> x :: s :: intersperse s xs
 
 let schedule entry (c : code) =
   let c' = PTree.map1 gather_bb_constraints c in
-  let (_, (vars, constraints, types)) = gather_cfg_constraints ([], ([], "", "")) c' entry in
+  let _, (vars, constraints, types) =
+    gather_cfg_constraints ([], ([], "", "")) c' entry
+  in
   let oc = open_out "lpsolve.txt" in
   fprintf oc "min: ";
   List.iter (fprintf oc "%s") (intersperse " + " vars);
diff --git a/src/hls/ValueVal.v b/src/hls/ValueVal.v
new file mode 100644
index 0000000..e978782
--- /dev/null
+++ b/src/hls/ValueVal.v
@@ -0,0 +1,203 @@
+(*
+ * Vericert: Verified high-level synthesis.
+ * Copyright (C) 2020 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/>.
+ *)
+
+(* begin hide *)
+From bbv Require Import Word.
+From bbv Require HexNotation WordScope.
+From Coq Require Import ZArith.ZArith FSets.FMapPositive Lia.
+From compcert Require Export lib.Integers common.Values.
+From vericert Require Import Vericertlib.
+(* end hide *)
+
+(** * Value
+
+A [value] is a bitvector with a specific size. We are using the implementation
+of the bitvector by mit-plv/bbv, because it has many theorems that we can reuse.
+However, we need to wrap it with an [Inductive] so that we can specify and match
+on the size of the [value]. This is necessary so that we can easily store
+[value]s of different sizes in a list or in a map.
+
+Using the default [word], this would not be possible, as the size is part of the type. *)
+
+Definition value : Type := val.
+
+(** ** Value conversions
+
+Various conversions to different number types such as [N], [Z], [positive] and
+[int], where the last one is a theory of integers of powers of 2 in CompCert. *)
+
+Definition valueToNat (v : value) : nat := .
+
+Definition natToValue (n : nat) : value :=
+  value_int (Int.repr (Z.of_nat n)).
+
+Definition natToValue64 (n : nat) : value :=
+  value_int64 (Int64.repr (Z.of_nat n)).
+
+Definition valueToN (v : value) : N :=
+  match v with
+  | value_bool b => N.b2n b
+  | value_int i => Z.to_N (Int.unsigned i)
+  | value_int64 i => Z.to_N (Int64.unsigned i)
+  end.
+
+Definition NToValue (n : N) : value :=
+  value_int (Int.repr (Z.of_N n)).
+
+Definition NToValue64 (n : N) : value :=
+  value_int64 (Int64.repr (Z.of_N n)).
+
+Definition ZToValue (z : Z) : value :=
+  value_int (Int.repr z).
+
+Definition ZToValue64 (z : Z) : value :=
+  value_int64 (Int64.repr z).
+
+Definition valueToZ (v : value) : Z :=
+  match v with
+  | value_bool b => Z.b2z b
+  | value_int i => Int.signed i
+  | value_int64 i => Int64.signed i
+  end.
+
+Definition uvalueToZ (v : value) : Z :=
+  match v with
+  | value_bool b => Z.b2z b
+  | value_int i => Int.unsigned i
+  | value_int64 i => Int64.unsigned i
+  end.
+
+Definition posToValue (p : positive) : value :=
+  value_int (Int.repr (Z.pos p)).
+
+Definition posToValue64 (p : positive) : value :=
+  value_int64 (Int64.repr (Z.pos p)).
+
+Definition valueToPos (v : value) : positive :=
+  match v with
+  | value_bool b => 1%positive
+  | value_int i => Z.to_pos (Int.unsigned i)
+  | value_int64 i => Z.to_pos (Int64.unsigned i)
+  end.
+
+Definition intToValue (i : Integers.int) : value := value_int i.
+
+Definition int64ToValue (i : Integers.int64) : value := value_int64 i.
+
+Definition valueToInt (v : value) : Integers.int :=
+  match v with
+  | value_bool b => Int.repr (if b then 1 else 0)
+  | value_int i => i
+  | value_int64 i => Int.repr (Int64.unsigned i)
+  end.
+
+(*Definition ptrToValue (i : ptrofs) : value :=
+  value_int (Ptrofs.to_int i).
+
+Definition valueToPtr (i : value) : Integers.ptrofs :=
+  Ptrofs.of_int i.
+
+Definition valToValue (v : Values.val) : option value :=
+  match v with
+  | Values.Vint i => Some (intToValue i)
+  | Values.Vint64 i => Some (intToValue i)
+  | Values.Vptr b off => Some (ptrToValue off)
+  | Values.Vundef => Some (ZToValue 0%Z)
+  | _ => None
+  end.
+
+(** Convert a [value] to a [bool], so that choices can be made based on the
+result. This is also because comparison operators will give back [value] instead
+of [bool], so if they are in a condition, they will have to be converted before
+they can be used. *)
+
+Definition valueToBool (v : value) : bool :=
+  if Z.eqb (uvalueToZ v) 0 then false else true.
+
+Definition boolToValue (b : bool) : value :=
+  natToValue (if b then 1 else 0).
+
+(** ** Arithmetic operations *)
+
+Definition unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1.
+intros; subst; assumption. Defined.
+
+Lemma unify_word_unfold :
+  forall sz w,
+  unify_word sz sz w eq_refl = w.
+Proof. auto. Qed.
+
+Inductive val_value_lessdef: val -> value -> Prop :=
+| val_value_lessdef_int:
+    forall i v',
+    i = valueToInt v' ->
+    val_value_lessdef (Vint i) v'
+| val_value_lessdef_ptr:
+    forall b off v',
+    off = valueToPtr v' ->
+    val_value_lessdef (Vptr b off) v'
+| lessdef_undef: forall v, val_value_lessdef Vundef v.
+
+Inductive opt_val_value_lessdef: option val -> value -> Prop :=
+| opt_lessdef_some:
+    forall v v', val_value_lessdef v v' -> opt_val_value_lessdef (Some v) v'
+| opt_lessdef_none: forall v, opt_val_value_lessdef None v.
+
+Lemma valueToZ_ZToValue :
+  forall z,
+  (Int.min_signed <= z <= Int.max_signed)%Z ->
+  valueToZ (ZToValue z) = z.
+Proof. auto using Int.signed_repr. Qed.
+
+Lemma uvalueToZ_ZToValue :
+  forall z,
+  (0 <= z <= Int.max_unsigned)%Z ->
+  uvalueToZ (ZToValue z) = z.
+Proof. auto using Int.unsigned_repr. Qed.
+
+Lemma valueToPos_posToValue :
+  forall v,
+  0 <= Z.pos v <= Int.max_unsigned ->
+  valueToPos (posToValue v) = v.
+Proof.
+  unfold valueToPos, posToValue.
+  intros. rewrite Int.unsigned_repr.
+  apply Pos2Z.id. assumption.
+Qed.
+
+Lemma valueToInt_intToValue :
+  forall v,
+  valueToInt (intToValue v) = v.
+Proof. auto. Qed.
+
+Lemma valToValue_lessdef :
+  forall v v',
+    valToValue v = Some v' ->
+    val_value_lessdef v v'.
+Proof.
+  intros.
+  destruct v; try discriminate; constructor.
+  unfold valToValue in H. inversion H.
+  unfold valueToInt. unfold intToValue in H1. auto.
+  inv H. symmetry. unfold valueToPtr, ptrToValue. apply Ptrofs.of_int_to_int. trivial.
+Qed.
+
+Ltac simplify_val := repeat (simplify; unfold uvalueToZ, valueToPtr, Ptrofs.of_int, valueToInt, intToValue,
+                                       ptrToValue in *)
+
+(*Ltac crush_val := simplify_val; try discriminate; try congruence; try lia; liapp; try assumption.*)
diff --git a/test/array.c b/test/array.c
index 7d78a61..5c80694 100644
--- a/test/array.c
+++ b/test/array.c
@@ -2,6 +2,6 @@ int main() {
     int x[3] = {1, 2, 3};
     int sum = 0, incr = 1;
     for (int i = 0; i < 3; i=i+incr)
-        sum += x[i];
+        sum = sum + i;
     return sum;
 }
diff --git a/test/loop.c b/test/loop.c
index 52e4fe9..bece7f2 100644
--- a/test/loop.c
+++ b/test/loop.c
@@ -1,10 +1,9 @@
 int main() {
     int max = 5;
     int acc = 0;
-    int b = 1;
     int c = 2;
     
-    for (int i = 0; i < max; i = i + b) {
+    for (int i = 0; i < max; i++) {
         acc += i;
     }