Merge branch 'develop' into dev-nadesh

10 files changed, 340 insertions, 39 deletions

diff --git a/Makefile b/Makefile
index 3d31b2f..1303b13 100644
--- a/Makefile
+++ b/Makefile
@@ -67,3 +67,4 @@ clean:: Makefile.coq
 
 clean::
 	rm -f */*.v.d */*.glob */*.vo */*~ *~
+	rm -f src/extraction/*.ml src/extraction/*.mli
diff --git a/driver/CoqupDriver.ml b/driver/CoqupDriver.ml
index 2932a50..afbe4d0 100644
--- a/driver/CoqupDriver.ml
+++ b/driver/CoqupDriver.ml
@@ -36,11 +36,7 @@ open Coqup.Frontend
 open Coqup.Assembler
 open Coqup.Linker
 open Coqup.Diagnostics
-
-(* Coqup flags *)
-let option_simulate = ref false
-let option_hls = ref true
-let option_debug_hls = ref false
+open Coqup.CoqupClflags
 
 (* Name used for version string etc. *)
 let tool_name = "C verified high-level synthesis"
@@ -215,6 +211,7 @@ Processing options:
   --no-hls       Do not use HLS and generate standard flow.
   --simulate     Simulate the result with the Verilog semantics.
   --debug-hls    Add debug logic to the Verilog.
+  --initialise-stack initialise the stack to all 0s.
 |} ^
   prepro_help ^
   language_support_help ^
@@ -316,6 +313,7 @@ let cmdline_actions =
   [Exact "--no-hls", Unset option_hls;
    Exact "--simulate", Set option_simulate;
    Exact "--debug-hls", Set option_debug_hls;
+   Exact "--initialise-stack", Set option_initial;
   ]
 (* Getting version info *)
   @ version_options tool_name @
diff --git a/src/CoqupClflags.ml b/src/CoqupClflags.ml
new file mode 100644
index 0000000..83dd31d
--- /dev/null
+++ b/src/CoqupClflags.ml
@@ -0,0 +1,5 @@
+(* Coqup flags *)
+let option_simulate = ref false
+let option_hls = ref true
+let option_debug_hls = ref false
+let option_initial = ref false
diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v
index 8df70d9..7d3156b 100644
--- a/src/common/IntegerExtra.v
+++ b/src/common/IntegerExtra.v
@@ -143,7 +143,7 @@ Module PtrofsExtra.
   Lemma divu_unsigned :
     forall x y,
       0 < Ptrofs.unsigned y ->
-      Ptrofs.unsigned x < Ptrofs.max_unsigned ->
+      Ptrofs.unsigned x <= Ptrofs.max_unsigned ->
       Ptrofs.unsigned (Ptrofs.divu x y) = Ptrofs.unsigned x / Ptrofs.unsigned y.
   Proof.
     intros.
@@ -154,7 +154,7 @@ Module PtrofsExtra.
     apply Ptrofs.unsigned_range.
     apply Z.div_le_upper_bound; auto.
     eapply Z.le_trans.
-    apply Z.lt_le_incl. exact H0.
+    exact H0.
     rewrite Z.mul_comm.
     apply Z.le_mul_diag_r; simplify; lia.
   Qed.
diff --git a/src/common/ZExtra.v b/src/common/ZExtra.v
new file mode 100644
index 0000000..a0dd717
--- /dev/null
+++ b/src/common/ZExtra.v
@@ -0,0 +1,34 @@
+Require Import ZArith.
+Require Import Lia.
+
+Local Open Scope Z_scope.
+
+Module ZExtra.
+
+  Lemma mod_0_bounds :
+    forall x y m,
+      0 < m ->
+      x mod m = 0 ->
+      y mod m = 0 ->
+      x <> y ->
+      x + m > y ->
+      y + m <= x.
+  Proof.
+    intros x y m.
+    intros POS XMOD YMOD NEQ H.
+    destruct (Z_le_gt_dec (y + m) x); eauto.
+
+    apply Znumtheory.Zmod_divide in YMOD; try lia.
+    apply Znumtheory.Zmod_divide in XMOD; try lia.
+    inversion XMOD as [x']; subst; clear XMOD.
+    inversion YMOD as [y']; subst; clear YMOD.
+
+    assert (x' <> y') as NEQ' by lia; clear NEQ.
+
+    rewrite <- Z.mul_succ_l in H.
+    rewrite <- Z.mul_succ_l in g.
+    apply Zmult_gt_reg_r in H;
+      apply Zmult_gt_reg_r in g; lia.
+  Qed.
+
+End ZExtra.
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 3665775..dfacb5e 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -18,7 +18,7 @@
 
 From compcert Require RTL Registers AST Integers.
 From compcert Require Import Globalenvs Memory.
-From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap Array IntegerExtra.
+From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap Array IntegerExtra ZExtra.
 From coqup Require HTL Verilog.
 
 Require Import Lia.
@@ -76,6 +76,13 @@ Definition arr_stack_based_pointers (spb : Values.block) (m : mem) (stack_length
                               (Values.Val.offset_ptr sp (Integers.Ptrofs.repr (4 * ptr)))))
                 spb.
 
+Definition stack_bounds (sp : Values.val) (hi : Z) (m : mem) : Prop :=
+  forall ptr v,
+    hi <= ptr <= Integers.Ptrofs.max_unsigned ->
+    Z.modulo ptr 4 = 0 ->
+    Mem.loadv AST.Mint32 m (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr )) = None /\
+    Mem.storev AST.Mint32 m (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr )) v = None.
+
 Inductive match_stacks (mem : mem) : list RTL.stackframe -> list HTL.stackframe -> Prop :=
 | match_stacks_nil :
     match_stacks mem nil nil
@@ -87,7 +94,8 @@ Inductive match_stacks (mem : mem) : list RTL.stackframe -> list HTL.stackframe
            (MARR : match_arrs m f sp mem asa)
            (SP : sp = Values.Vptr sp' (Integers.Ptrofs.repr 0))
            (RSBP: reg_stack_based_pointers sp' rs)
-           (ASBP: arr_stack_based_pointers sp' mem (f.(RTL.fn_stacksize)) sp),
+           (ASBP: arr_stack_based_pointers sp' mem (f.(RTL.fn_stacksize)) sp)
+           (BOUNDS : stack_bounds sp (f.(RTL.fn_stacksize)) mem),
       match_stacks mem (RTL.Stackframe r f sp pc rs :: cs)
                        (HTL.Stackframe r m pc asr asa :: lr).
 
@@ -99,8 +107,9 @@ Inductive match_states : RTL.state -> HTL.state -> Prop :=
     (MS : match_stacks mem sf res)
     (MARR : match_arrs m f sp mem asa)
     (SP : sp = Values.Vptr sp' (Integers.Ptrofs.repr 0))
-    (RSBP: reg_stack_based_pointers sp' rs)
-    (ASBP: arr_stack_based_pointers sp' mem (f.(RTL.fn_stacksize)) sp),
+    (RSBP : reg_stack_based_pointers sp' rs)
+    (ASBP : arr_stack_based_pointers sp' mem (f.(RTL.fn_stacksize)) sp)
+    (BOUNDS : stack_bounds sp (f.(RTL.fn_stacksize)) mem),
     match_states (RTL.State sf f sp st rs mem)
                  (HTL.State res m st asr asa)
 | match_returnstate :
@@ -601,9 +610,6 @@ Section CORRECTNESS.
         remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0))
                                       (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET.
 
-        (** Read bounds assumption *)
-        assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit.
-
         (** Modular preservation proof *)
         assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
         { rewrite HeqOFFSET.
@@ -615,6 +621,18 @@ Section CORRECTNESS.
           rewrite Integers.Int.signed_repr; simplify; try split; try assumption.
         }
 
+        (** Read bounds proof *)
+        assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH.
+        { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; simplify; auto.
+          unfold stack_bounds in BOUNDS.
+          exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); auto.
+          split; try lia; apply Integers.Ptrofs.unsigned_range_2.
+          simplify.
+          replace (Integers.Ptrofs.repr 0) with (Integers.Ptrofs.zero) by reflexivity.
+          rewrite Integers.Ptrofs.add_zero_l.
+          rewrite Integers.Ptrofs.unsigned_repr. intros. simplify. congruence.
+          apply Integers.Ptrofs.unsigned_range_2. }
+
         (** Normalisation proof *)
         assert (Integers.Ptrofs.repr
                   (4 * Integers.Ptrofs.unsigned
@@ -808,9 +826,6 @@ Section CORRECTNESS.
                                          (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z))
                                                            (Integers.Int.repr z0)))) as OFFSET.
 
-        (** Read bounds assumption *)
-        assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit.
-
         (** Modular preservation proof *)
         assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
         { rewrite HeqOFFSET.
@@ -828,6 +843,18 @@ Section CORRECTNESS.
           rewrite Integers.Int.signed_repr; simplify; try split; try assumption.
         }
 
+        (** Read bounds proof *)
+        assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH.
+        { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; simplify; auto.
+          unfold stack_bounds in BOUNDS.
+          exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); auto.
+          split; try lia; apply Integers.Ptrofs.unsigned_range_2.
+          simplify.
+          replace (Integers.Ptrofs.repr 0) with (Integers.Ptrofs.zero) by reflexivity.
+          rewrite Integers.Ptrofs.add_zero_l.
+          rewrite Integers.Ptrofs.unsigned_repr. intros. simplify. congruence.
+          apply Integers.Ptrofs.unsigned_range_2. }
+
         (** Normalisation proof *)
         assert (Integers.Ptrofs.repr
                   (4 * Integers.Ptrofs.unsigned
@@ -1001,12 +1028,20 @@ Section CORRECTNESS.
 
         remember i0 as OFFSET.
 
-        (** Read bounds assumption *)
-        assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit.
-
         (** Modular preservation proof *)
         rename H0 into MOD_PRESERVE.
 
+        (** Read bounds proof *)
+        assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH.
+        { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; simplify; auto.
+          unfold stack_bounds in BOUNDS.
+          exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); auto.
+          simplify.
+          replace (Integers.Ptrofs.repr 0) with (Integers.Ptrofs.zero) by reflexivity.
+          rewrite Integers.Ptrofs.add_zero_l.
+          rewrite Integers.Ptrofs.unsigned_repr. intros. simplify. congruence.
+          apply Integers.Ptrofs.unsigned_range_2. }
+
         (** Normalisation proof *)
         assert (Integers.Ptrofs.repr
                   (4 * Integers.Ptrofs.unsigned
@@ -1187,9 +1222,6 @@ Section CORRECTNESS.
         remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0))
                                       (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET.
 
-        (** Read bounds assumption *)
-        assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH by admit.
-
         (** Modular preservation proof *)
         assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
         { rewrite HeqOFFSET.
@@ -1201,6 +1233,18 @@ Section CORRECTNESS.
           rewrite Integers.Int.signed_repr; simplify; try split; try assumption.
         }
 
+        (** Write bounds proof *)
+        assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH.
+        { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; simplify; auto.
+          unfold stack_bounds in BOUNDS.
+          exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); auto.
+          split; try lia; apply Integers.Ptrofs.unsigned_range_2.
+          simplify.
+          replace (Integers.Ptrofs.repr 0) with (Integers.Ptrofs.zero) by reflexivity.
+          rewrite Integers.Ptrofs.add_zero_l.
+          rewrite Integers.Ptrofs.unsigned_repr. intros. simplify. congruence.
+          apply Integers.Ptrofs.unsigned_range_2. }
+
         (** Start of proof proper *)
         eexists. split.
         eapply Smallstep.plus_one.
@@ -1353,7 +1397,7 @@ Section CORRECTNESS.
         intro.
         apply Z2Nat.inj_iff in H14; try lia.
         apply Z.div_pos; try lia.
-        apply Integers.Ptrofs.unsigned_range.
+        apply Integers.Ptrofs.unsigned_range_2.
 
         assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
         unfold arr_stack_based_pointers.
@@ -1371,8 +1415,7 @@ Section CORRECTNESS.
         simplify.
         destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor.
         destruct (Archi.ptr64); try discriminate.
-        pose proof (RSBP src). rewrite EQ_SRC in H0.
-        assumption.
+        pose proof (RSBP src). rewrite EQ_SRC in H0. assumption.
 
         simpl.
         erewrite Mem.load_store_other with (m1 := m).
@@ -1394,6 +1437,33 @@ Section CORRECTNESS.
         }
         apply ASBP; assumption.
 
+        unfold stack_bounds in *. intros.
+        simpl.
+        assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+        erewrite Mem.load_store_other with (m1 := m).
+        2: { exact H1. }
+        2: { right. right. simpl.
+             rewrite ZERO.
+             rewrite Integers.Ptrofs.add_zero_l.
+             rewrite Integers.Ptrofs.unsigned_repr; simplify; try lia.
+             apply ZExtra.mod_0_bounds; simplify; try lia. }
+        simplify. split.
+        exploit (BOUNDS ptr); try lia. intros. simplify. assumption.
+        exploit (BOUNDS ptr v); try lia. intros.
+        invert H0.
+        match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity.
+        assert (Mem.valid_access m AST.Mint32 sp'
+                                 (Integers.Ptrofs.unsigned
+                                    (Integers.Ptrofs.add (Integers.Ptrofs.repr 0)
+                                                         (Integers.Ptrofs.repr ptr))) Writable).
+        { pose proof H1. eapply Mem.store_valid_access_2 in H0.
+          exact H0. eapply Mem.store_valid_access_3. eassumption. }
+        pose proof (Mem.valid_access_store m AST.Mint32 sp'
+                                           (Integers.Ptrofs.unsigned
+                                              (Integers.Ptrofs.add (Integers.Ptrofs.repr 0)
+                                                                   (Integers.Ptrofs.repr ptr))) v).
+        apply X in H0. invert H0. congruence.
+
       + (** Preamble *)
         invert MARR. simplify.
 
@@ -1435,9 +1505,6 @@ Section CORRECTNESS.
                                          (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z))
                                                            (Integers.Int.repr z0)))) as OFFSET.
 
-        (** Read bounds assumption *)
-        assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit.
-
         (** Modular preservation proof *)
         assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
         { rewrite HeqOFFSET.
@@ -1455,6 +1522,18 @@ Section CORRECTNESS.
           rewrite Integers.Int.signed_repr; simplify; try split; try assumption.
         }
 
+        (** Write bounds proof *)
+        assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH.
+        { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; simplify; auto.
+          unfold stack_bounds in BOUNDS.
+          exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); auto.
+          split; try lia; apply Integers.Ptrofs.unsigned_range_2.
+          simplify.
+          replace (Integers.Ptrofs.repr 0) with (Integers.Ptrofs.zero) by reflexivity.
+          rewrite Integers.Ptrofs.add_zero_l.
+          rewrite Integers.Ptrofs.unsigned_repr. intros. simplify. congruence.
+          apply Integers.Ptrofs.unsigned_range_2. }
+
         (** Start of proof proper *)
         eexists. split.
         eapply Smallstep.plus_one.
@@ -1653,6 +1732,33 @@ Section CORRECTNESS.
         }
         apply ASBP; assumption.
 
+        unfold stack_bounds in *. intros.
+        simpl.
+        assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+        erewrite Mem.load_store_other with (m1 := m).
+        2: { exact H1. }
+        2: { right. right. simpl.
+             rewrite ZERO.
+             rewrite Integers.Ptrofs.add_zero_l.
+             rewrite Integers.Ptrofs.unsigned_repr; simplify; try lia.
+             apply ZExtra.mod_0_bounds; simplify; try lia. }
+        simplify. split.
+        exploit (BOUNDS ptr); try lia. intros. simplify. assumption.
+        exploit (BOUNDS ptr v); try lia. intros.
+        invert H0.
+        match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity.
+        assert (Mem.valid_access m AST.Mint32 sp'
+                                 (Integers.Ptrofs.unsigned
+                                    (Integers.Ptrofs.add (Integers.Ptrofs.repr 0)
+                                                         (Integers.Ptrofs.repr ptr))) Writable).
+        { pose proof H1. eapply Mem.store_valid_access_2 in H0.
+          exact H0. eapply Mem.store_valid_access_3. eassumption. }
+        pose proof (Mem.valid_access_store m AST.Mint32 sp'
+                                           (Integers.Ptrofs.unsigned
+                                              (Integers.Ptrofs.add (Integers.Ptrofs.repr 0)
+                                                                   (Integers.Ptrofs.repr ptr))) v).
+        apply X in H0. invert H0. congruence.
+
       + invert MARR. simplify.
 
         unfold Op.eval_addressing in H0.
@@ -1668,12 +1774,20 @@ Section CORRECTNESS.
 
         remember i0 as OFFSET.
 
-        (** Read bounds assumption *)
-        assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit.
-
         (** Modular preservation proof *)
         rename H0 into MOD_PRESERVE.
 
+        (** Write bounds proof *)
+        assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH.
+        { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; simplify; auto.
+          unfold stack_bounds in BOUNDS.
+          exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); auto.
+          simplify.
+          replace (Integers.Ptrofs.repr 0) with (Integers.Ptrofs.zero) by reflexivity.
+          rewrite Integers.Ptrofs.add_zero_l.
+          rewrite Integers.Ptrofs.unsigned_repr. intros. simplify. congruence.
+          apply Integers.Ptrofs.unsigned_range_2. }
+
         (** Start of proof proper *)
         eexists. split.
         eapply Smallstep.plus_one.
@@ -1861,6 +1975,33 @@ Section CORRECTNESS.
         }
         apply ASBP; assumption.
 
+        unfold stack_bounds in *. intros.
+        simpl.
+        assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+        erewrite Mem.load_store_other with (m1 := m).
+        2: { exact H1. }
+        2: { right. right. simpl.
+             rewrite ZERO.
+             rewrite Integers.Ptrofs.add_zero_l.
+             rewrite Integers.Ptrofs.unsigned_repr; simplify; try lia.
+             apply ZExtra.mod_0_bounds; simplify; try lia. }
+        simplify. split.
+        exploit (BOUNDS ptr); try lia. intros. simplify. assumption.
+        exploit (BOUNDS ptr v); try lia. intros.
+        invert H0.
+        match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity.
+        assert (Mem.valid_access m AST.Mint32 sp'
+                                 (Integers.Ptrofs.unsigned
+                                    (Integers.Ptrofs.add (Integers.Ptrofs.repr 0)
+                                                         (Integers.Ptrofs.repr ptr))) Writable).
+        { pose proof H1. eapply Mem.store_valid_access_2 in H0.
+          exact H0. eapply Mem.store_valid_access_3. eassumption. }
+        pose proof (Mem.valid_access_store m AST.Mint32 sp'
+                                           (Integers.Ptrofs.unsigned
+                                              (Integers.Ptrofs.add (Integers.Ptrofs.repr 0)
+                                                                   (Integers.Ptrofs.repr ptr))) v).
+        apply X in H0. invert H0. congruence.
+
     - eexists. split. apply Smallstep.plus_one.
       eapply HTL.step_module; eauto.
       apply assumption_32bit.
@@ -2090,6 +2231,49 @@ Section CORRECTNESS.
       repeat constructor.
       constructor.
 
+      Transparent Mem.alloc. (* TODO: Since there are opaque there's probably a lemma. *)
+      Transparent Mem.load.
+      Transparent Mem.store.
+      unfold stack_bounds.
+      split.
+
+      unfold Mem.alloc in H.
+      invert H.
+      simplify.
+      unfold Mem.load.
+      intros.
+      match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence.
+      invert v0. unfold Mem.range_perm in H3.
+      unfold Mem.perm in H3. simplify.
+      unfold Mem.perm_order' in H3.
+      rewrite Integers.Ptrofs.add_zero_l in H3.
+      rewrite Integers.Ptrofs.unsigned_repr in H3; simplify; try lia.
+      exploit (H3 ptr). lia. intros.
+      rewrite Maps.PMap.gss in H8.
+      match goal with | H8 : context[if ?x then _ else _] |- _ => destruct x eqn:EQ end; try contradiction.
+      simplify.
+      apply proj_sumbool_true in H10. lia.
+
+      unfold Mem.alloc in H.
+      invert H.
+      simplify.
+      unfold Mem.store.
+      intros.
+      match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence.
+      invert v0. unfold Mem.range_perm in H3.
+      unfold Mem.perm in H3. simplify.
+      unfold Mem.perm_order' in H3.
+      rewrite Integers.Ptrofs.add_zero_l in H3.
+      rewrite Integers.Ptrofs.unsigned_repr in H3; simplify; try lia.
+      exploit (H3 ptr). lia. intros.
+      rewrite Maps.PMap.gss in H8.
+      match goal with | H8 : context[if ?x then _ else _] |- _ => destruct x eqn:EQ end; try contradiction.
+      simplify.
+      apply proj_sumbool_true in H10. lia.
+      Opaque Mem.alloc.
+      Opaque Mem.load.
+      Opaque Mem.store.
+
     - invert MSTATE. invert MS.
       econstructor.
       split. apply Smallstep.plus_one.
@@ -2116,7 +2300,6 @@ Section CORRECTNESS.
   Admitted.
   Hint Resolve transl_step_correct : htlproof.
 
-
   Lemma option_inv :
     forall A x y,
       @Some A x = Some y -> x = y.
diff --git a/src/translation/Veriloggenproof.v b/src/translation/Veriloggenproof.v
index 518fe3a..ca4ecab 100644
--- a/src/translation/Veriloggenproof.v
+++ b/src/translation/Veriloggenproof.v
@@ -69,10 +69,10 @@ Section CORRECTNESS.
         match_states S1 R1 ->
         exists R2, Smallstep.plus step tge R1 t R2 /\ match_states S2 R2.
   Proof.
-    induction 1; intros R1 MSTATE; inv MSTATE; econstructor; split.
+(*    induction 1; intros R1 MSTATE; inv MSTATE; econstructor; split.
     - apply Smallstep.plus_one. econstructor. eassumption. trivial.
-      * econstructor. econstructor.
-        Admitted.
+      * econstructor. econstructor.*)
+    Admitted.
 
   Theorem transf_program_correct:
     forward_simulation (HTL.semantics prog) (Verilog.semantics tprog).
diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml
index 5dc0386..6d10887 100644
--- a/src/verilog/PrintVerilog.ml
+++ b/src/verilog/PrintVerilog.ml
@@ -22,9 +22,12 @@ open Datatypes
 
 open Camlcoq
 open AST
+open Clflags
 
 open Printf
 
+open CoqupClflags
+
 let concat = String.concat ""
 
 let indent i = String.make (2 * i) ' '
@@ -187,6 +190,12 @@ let debug_always i clk state = concat [
     indent i; "end\n"
   ]
 
+let print_initial i n stk = concat [
+    indent i; "integer i;\n";
+    indent i; "initial for(i = 0; i < "; sprintf "%d" n; "; i++)\n";
+    indent (i+1); register stk; "[i] = 0;\n"
+  ]
+
 let pprint_module debug i n m =
   if (extern_atom n) = "main" then
     let inputs = m.mod_start :: m.mod_reset :: m.mod_clk :: m.mod_args in
@@ -194,6 +203,7 @@ let pprint_module debug i n m =
     concat [ indent i; "module "; (extern_atom n);
              "("; concat (intersperse ", " (List.map register (inputs @ outputs))); ");\n";
              fold_map (pprint_module_item (i+1)) m.mod_body;
+             if !option_initial then print_initial i (Nat.to_int m.mod_stk_len) m.mod_stk else "";
              if debug then debug_always i m.mod_clk m.mod_st else "";
              indent i; "endmodule\n\n"
            ]
diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index e7b2362..8ba5138 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -108,6 +108,11 @@ Definition boolToValue (sz : nat) (b : bool) : value :=
 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.
+
 Definition value_eq_size:
   forall v1 v2 : value, { vsize v1 = vsize v2 } + { True }.
 Proof.
@@ -324,6 +329,12 @@ Proof.
   auto using uwordToZ_ZToWord.
 Qed.
 
+Lemma uvalueToZ_ZToValue_full :
+  forall sz : nat,
+  (0 < sz)%nat ->
+  forall z : Z, uvalueToZ (ZToValue sz z) = (z mod 2 ^ Z.of_nat sz)%Z.
+Proof. unfold uvalueToZ, ZToValue. simpl. auto using uwordToZ_ZToWord_full. Qed.
+
 Lemma ZToValue_uvalueToZ :
   forall v,
   ZToValue (vsize v) (uvalueToZ v) = v.
@@ -382,7 +393,64 @@ Qed.
 Lemma boolToValue_ValueToBool :
   forall b,
   valueToBool (boolToValue 32 b) = b.
-Proof. destruct b; unfold valueToBool, boolToValue; simpl; trivial. Qed.
+Proof. destruct b; auto. Qed.
+
+Local Open Scope Z.
+
+Ltac word_op_value H :=
+  intros; unfold uvalueToZ, ZToValue; simpl; rewrite unify_word_unfold;
+  rewrite <- H; rewrite uwordToZ_ZToWord_full; auto; omega.
+
+Lemma zadd_vplus :
+  forall sz z1 z2,
+  (sz > 0)%nat ->
+  uvalueToZ (vplus (ZToValue sz z1) (ZToValue sz z2) eq_refl) = (z1 + z2) mod 2 ^ Z.of_nat sz.
+Proof. word_op_value ZToWord_plus. Qed.
+
+Lemma zadd_vplus2 :
+  forall z1 z2,
+  vplus (ZToValue 32 z1) (ZToValue 32 z2) eq_refl = ZToValue 32 (z1 + z2).
+Proof.
+  intros. unfold vplus, ZToValue, map_word2. rewrite unify_word_unfold. simpl.
+  rewrite ZToWord_plus; auto.
+Qed.
+
+Lemma wordsize_32 :
+  Int.wordsize = 32%nat.
+Proof. auto. Qed.
+
+Lemma intadd_vplus :
+  forall i1 i2,
+  valueToInt (vplus (intToValue i1) (intToValue i2) eq_refl) = Int.add i1 i2.
+Proof.
+  intros. unfold Int.add, valueToInt, intToValue. rewrite zadd_vplus.
+  rewrite <- Int.unsigned_repr_eq.
+  rewrite Int.repr_unsigned. auto. rewrite wordsize_32. omega.
+Qed.
+
+Lemma zsub_vminus :
+  forall sz z1 z2,
+  (sz > 0)%nat ->
+  uvalueToZ (vminus (ZToValue sz z1) (ZToValue sz z2) eq_refl) = (z1 - z2) mod 2 ^ Z.of_nat sz.
+Proof. word_op_value ZToWord_minus. Qed.
+
+Lemma zmul_vmul :
+  forall sz z1 z2,
+  (sz > 0)%nat ->
+  uvalueToZ (vmul (ZToValue sz z1) (ZToValue sz z2) eq_refl) = (z1 * z2) mod 2 ^ Z.of_nat sz.
+Proof. word_op_value ZToWord_mult. Qed.
+
+Local Open Scope N.
+Lemma zdiv_vdiv :
+  forall n1 n2,
+  n1 < 2 ^ 32 ->
+  n2 < 2 ^ 32 ->
+  n1 / n2 < 2 ^ 32 ->
+  valueToN (vdiv (NToValue 32 n1) (NToValue 32 n2) eq_refl) = n1 / n2.
+Proof.
+  intros; unfold valueToN, NToValue; simpl; rewrite unify_word_unfold. unfold wdiv.
+  unfold wordBin. repeat (rewrite wordToN_NToWord_2); auto.
+Qed.
 
 (*Lemma ZToValue_valueToNat :
   forall x sz,
diff --git a/test/loop.c b/test/loop.c
index b459e3a..52e4fe9 100644
--- a/test/loop.c
+++ b/test/loop.c
@@ -1,10 +1,12 @@
 int main() {
     int max = 5;
     int acc = 0;
+    int b = 1;
+    int c = 2;
     
-    for (int i = 0; i < max; i++) {
+    for (int i = 0; i < max; i = i + b) {
         acc += i;
     }
 
-    return acc + 2;
+    return acc + c;
 }