Merge remote-tracking branch 'james/arrays-proof' into develop

9 files changed, 725 insertions, 111 deletions

diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v
index 47360d6..efa1323 100644
--- a/src/common/Coquplib.v
+++ b/src/common/Coquplib.v
@@ -41,6 +41,19 @@ Ltac solve_by_inverts n :=
 
 Ltac solve_by_invert := solve_by_inverts 1.
 
+Ltac invert x := inversion x; subst; clear x.
+
+Ltac clear_obvious :=
+  repeat match goal with
+         | [ H : ex _ |- _ ] => invert H
+         | [ H : ?C _ = ?C _ |- _ ] => invert H
+         | [ H : _ /\ _ |- _ ] => invert H
+         end.
+
+Ltac simplify := simpl in *; clear_obvious; simpl in *; try discriminate.
+
+Global Opaque Nat.div.
+
 (* Definition const (A B : Type) (a : A) (b : B) : A := a.
 
 Definition compose (A B C : Type) (f : B -> C) (g : A -> B) (x : A) : C := f (g x). *)
@@ -71,6 +84,12 @@ Definition bind {A B : Type} (f : option A) (g : A -> option B) : option B :=
   | _ => None
   end.
 
+Definition join {A : Type} (a : option (option A)) : option A :=
+  match a with
+  | None => None
+  | Some a' => a'
+  end.
+
 Module Notation.
 Notation "'do' X <- A ; B" := (bind A (fun X => B))
    (at level 200, X ident, A at level 100, B at level 200).
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 11580cd..b26b9e3 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -131,7 +131,7 @@ Lemma declare_reg_state_incr :
        s.(st_st)
        s.(st_freshreg)
        s.(st_freshstate)
-       (AssocMap.set r (i, Scalar sz) s.(st_scldecls))
+       (AssocMap.set r (i, VScalar sz) s.(st_scldecls))
        s.(st_arrdecls)
        s.(st_datapath)
        s.(st_controllogic)).
@@ -142,7 +142,7 @@ Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit :=
                 s.(st_st)
                 s.(st_freshreg)
                 s.(st_freshstate)
-                (AssocMap.set r (i, Scalar sz) s.(st_scldecls))
+                (AssocMap.set r (i, VScalar sz) s.(st_scldecls))
                 s.(st_arrdecls)
                 s.(st_datapath)
                 s.(st_controllogic))
@@ -339,24 +339,24 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit :=
 
 Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing)
            (args : list reg) (stack : reg) : mon expr :=
-  match addr, args with (* TODO: We should be more methodical here; what are the possibilities?*)
-  | Op.Aindexed off, r1::nil => (* FIXME: Cannot guarantee alignment *)
+  match mem, addr, args with (* TODO: We should be more methodical here; what are the possibilities?*)
+  | Mint32, Op.Aindexed off, r1::nil => (* FIXME: Cannot guarantee alignment *)
     ret (Vvari stack (Vbinop Vadd (boplitz Vdiv r1 4) (Vlit (ZToValue 32 (off / 4)))))
-  | Op.Ascaled scale offset, r1::nil =>
+  | Mint32, Op.Ascaled scale offset, r1::nil =>
     if ((Z.eqb (Z.modulo scale 4) 0) && (Z.eqb (Z.modulo offset 4) 0))
     then ret (Vvari stack (Vbinop Vadd (boplitz Vmul r1 (scale / 4)) (Vlit (ZToValue 32 (offset / 4)))))
     else error (Errors.msg "Htlgen: translate_arr_access address misaligned")
-  | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)
+  | Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)
     if ((Z.eqb (Z.modulo scale 4) 0) && (Z.eqb (Z.modulo offset 4) 0))
     then ret (Vvari stack
                     (Vbinop Vadd (Vbinop Vadd (boplitz Vdiv r1 4) (Vlit (ZToValue 32 (offset / 4))))
                                  (boplitz Vmul r2 (scale / 4))))
     else error (Errors.msg "Htlgen: translate_arr_access address misaligned")
-  | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)
+  | Mint32, Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)
     let a := Integers.Ptrofs.unsigned a in (* FIXME: Assuming stack offsets are +ve; is this ok? *)
     if (Z.eq_dec (Z.modulo a 4) 0) then ret (Vvari stack (Vlit (ZToValue 32 (a / 4))))
     else error (Errors.msg "Htlgen: eff_addressing misaligned stack offset")
-  | _, _ => error (Errors.msg "Htlgen: translate_arr_access unsupported addressing")
+  | _, _, _ => error (Errors.msg "Htlgen: translate_arr_access unsuported addressing")
   end.
 
 Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit :=
@@ -371,10 +371,10 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni
     | Iload mem addr args dst n' =>
       do src <- translate_arr_access mem addr args stack;
       do _ <- declare_reg None dst 32;
-      add_instr n n' (block dst src)
+      add_instr n n' (nonblock dst src)
     | Istore mem addr args src n' =>
       do dst <- translate_arr_access mem addr args stack;
-      add_instr n n' (Vblock dst (Vvar src)) (* TODO: Could juse use add_instr? reg exists. *)
+      add_instr n n' (Vnonblock dst (Vvar src)) (* TODO: Could juse use add_instr? reg exists. *)
     | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.")
     | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.")
     | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.")
@@ -398,7 +398,7 @@ Lemma create_reg_state_incr:
          s.(st_st)
          (Pos.succ (st_freshreg s))
          (st_freshstate s)
-         (AssocMap.set s.(st_freshreg) (i, Scalar sz) s.(st_scldecls))
+         (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls))
          s.(st_arrdecls)
          (st_datapath s)
          (st_controllogic s)).
@@ -410,7 +410,7 @@ Definition create_reg (i : option io) (sz : nat) : mon reg :=
                    s.(st_st)
                    (Pos.succ r)
                    (st_freshstate s)
-                   (AssocMap.set s.(st_freshreg) (i, Scalar sz) s.(st_scldecls))
+                   (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls))
                    (st_arrdecls s)
                    (st_datapath s)
                    (st_controllogic s))
@@ -423,27 +423,28 @@ Lemma create_arr_state_incr:
          (Pos.succ (st_freshreg s))
          (st_freshstate s)
          s.(st_scldecls)
-         (AssocMap.set s.(st_freshreg) (i, Array sz ln) s.(st_arrdecls))
+         (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 :=
+Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) :=
   fun s => let r := s.(st_freshreg) in
-           OK r (mkstate
+           OK (r, ln) (mkstate
                    s.(st_st)
                    (Pos.succ r)
                    (st_freshstate s)
                    s.(st_scldecls)
-                   (AssocMap.set s.(st_freshreg) (i, Array sz ln) s.(st_arrdecls))
+                   (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 transf_module (f: function) : mon module :=
+  if (Z.eq_dec (Z.modulo f.(fn_stacksize) 4) 0) then
   do fin <- create_reg (Some Voutput) 1;
   do rtrn <- create_reg (Some Voutput) 32;
-  do stack <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4));
+  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;
@@ -457,20 +458,22 @@ Definition transf_module (f: function) : mon module :=
          f.(fn_entrypoint)
          current_state.(st_st)
          stack
+         stack_len
          fin
          rtrn
          start
          rst
          clk
          current_state.(st_scldecls)
-         current_state.(st_arrdecls)).
+         current_state.(st_arrdecls))
+  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, Scalar 32) (st_scldecls (init_state st)))
+          (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)).
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 4b7f268..046ae06 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -18,9 +18,11 @@
 
 From compcert Require RTL Registers AST Integers.
 From compcert Require Import Globalenvs Memory.
-From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap.
+From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap Array.
 From coqup Require HTL Verilog.
 
+Require Import Lia.
+
 Local Open Scope assocmap.
 
 Hint Resolve Smallstep.forward_simulation_plus : htlproof.
@@ -42,44 +44,64 @@ Definition state_st_wf (m : HTL.module) (s : HTL.state) :=
   asa!(m.(HTL.mod_st)) = Some (posToValue 32 st).
 Hint Unfold state_st_wf : htlproof.
 
-Inductive match_stacks : list RTL.stackframe -> list HTL.stackframe -> Prop :=
+Inductive match_arrs (m : HTL.module) (f : RTL.function) (sp : Values.val) (mem : mem) :
+  Verilog.assocmap_arr -> Prop :=
+| match_arr : forall asa stack,
+    asa ! (m.(HTL.mod_stk)) = Some stack /\
+    stack.(arr_length) = Z.to_nat (f.(RTL.fn_stacksize) / 4) /\
+    (forall ptr,
+        0 <= ptr < Z.of_nat m.(HTL.mod_stk_len) ->
+        opt_val_value_lessdef (Mem.loadv AST.Mint32 mem
+                                         (Values.Val.offset_ptr sp (Integers.Ptrofs.repr (4 * ptr))))
+                              (Option.default (NToValue 32 0)
+                                 (Option.join (array_get_error (Z.to_nat ptr) stack)))) ->
+    match_arrs m f sp mem asa.
+
+Inductive match_stacks (mem : mem) : list RTL.stackframe -> list HTL.stackframe -> Prop :=
 | match_stacks_nil :
-    match_stacks nil nil
+    match_stacks mem nil nil
 | match_stacks_cons :
-    forall cs lr r f sp pc rs m assoc
+    forall cs lr r f sp pc rs m asr asa
            (TF : tr_module f m)
-           (ST: match_stacks cs lr)
-           (MA: match_assocmaps f rs assoc),
-      match_stacks (RTL.Stackframe r f sp pc rs :: cs)
-                   (HTL.Stackframe r m pc assoc :: lr).
-
-Inductive match_arrs (m : HTL.module) : RTL.function -> mem ->  AssocMap.t (list value) -> Prop :=
-| match_arr : forall mem asa stack sp f sz,
-    sz = f.(RTL.fn_stacksize) ->
-    asa ! (m.(HTL.mod_stk)) = Some stack ->
-    (forall ptr,
-        0 <= ptr < sz ->
-        nth_error stack (Z.to_nat ptr) =
-        (Coquplib.Option.bind (Mem.loadv AST.Mint32 mem
-                                         (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr)))
-         valToValue)) ->
-    match_arrs m f mem asa.
+           (ST: match_stacks mem cs lr)
+           (MA: match_assocmaps f rs asr)
+           (MARR : match_arrs m f sp mem asa),
+      match_stacks mem (RTL.Stackframe r f sp pc rs :: cs)
+                       (HTL.Stackframe r m pc asr asa :: lr).
+
+Definition reg_stack_based_pointers (sp : Values.block) (rs : Registers.Regmap.t Values.val) : Prop :=
+  forall r, match Registers.Regmap.get r rs with
+        | Values.Vptr sp' off => sp' = sp
+        | _ => True
+        end.
+
+Definition arr_stack_based_pointers (spb : Values.block) (m : mem) (stack_length : Z)
+  (sp : Values.val) : Prop :=
+  forall ptr,
+    0 <= ptr < (stack_length / 4) ->
+    match Mem.loadv AST.Mint32 m (Values.Val.offset_ptr sp (Integers.Ptrofs.repr (4 * ptr))) with
+    | Some (Values.Vptr sp' off) => sp' = spb
+    | _ => True
+    end.
 
 Inductive match_states : RTL.state -> HTL.state -> Prop :=
-| match_state : forall asa asr sf f sp rs mem m st res
+| match_state : forall asa asr sf f sp sp' rs mem m st res
     (MASSOC : match_assocmaps f rs asr)
     (TF : tr_module f m)
     (WF : state_st_wf m (HTL.State res m st asr asa))
-    (MS : match_stacks sf res)
-    (MA : match_arrs m f mem asa),
+    (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),
     match_states (RTL.State sf f sp st rs mem)
                  (HTL.State res m st asr asa)
 | match_returnstate :
     forall
-      v v' stack m res
-      (MS : match_stacks stack res),
+      v v' stack mem res
+      (MS : match_stacks mem stack res),
       val_value_lessdef v v' ->
-      match_states (RTL.Returnstate stack v m) (HTL.Returnstate res v')
+      match_states (RTL.Returnstate stack v mem) (HTL.Returnstate res v')
 | match_initial_call :
     forall f m m0
     (TF : tr_module f m),
@@ -129,6 +151,33 @@ Proof.
 Qed.
 Hint Resolve regs_lessdef_add_match : htlproof.
 
+Lemma list_combine_none :
+  forall n l,
+    length l = n ->
+    list_combine Verilog.merge_cell (list_repeat None n) l = l.
+Proof.
+  induction n; intros; simplify.
+  - symmetry. apply length_zero_iff_nil. auto.
+  - destruct l; simplify.
+    rewrite list_repeat_cons.
+    simplify. f_equal.
+    eauto.
+Qed.
+
+Lemma combine_none :
+  forall n a,
+    a.(arr_length) = n ->
+    arr_contents (combine Verilog.merge_cell (arr_repeat None n) a) = arr_contents a.
+Proof.
+  intros.
+  unfold combine.
+  simplify.
+
+  rewrite <- (arr_wf a) in H.
+  apply list_combine_none.
+  assumption.
+Qed.
+
 (* Need to eventually move posToValue 32 to posToValueAuto, as that has this proof. *)
 Lemma assumption_32bit :
   forall v,
@@ -297,21 +346,51 @@ Section CORRECTNESS.
       eapply HTL.step_module; eauto.
       (* processing of state *)
       econstructor.
-      simpl. trivial.
+      simplify.
       econstructor.
       econstructor.
       econstructor.
+      simplify.
 
-      (* prove stval *)
-      unfold merge_assocmap.
-      unfold_merge. simpl. apply AssocMap.gss.
+      unfold Verilog.merge_regs.
+      unfold_merge. apply AssocMap.gss.
 
       (* prove match_state *)
       rewrite assumption_32bit.
-      constructor; auto.
+      econstructor; simplify; eauto.
+
+      unfold Verilog.merge_regs.
       unfold_merge. simpl. apply regs_lessdef_add_greater. apply greater_than_max_func.
       assumption.
+      unfold Verilog.merge_regs.
       unfold state_st_wf. inversion 1. subst. unfold_merge. apply AssocMap.gss.
+
+      (* prove match_arrs *)
+      invert MARR. simplify.
+      unfold HTL.empty_stack. simplify. unfold Verilog.merge_arrs.
+      econstructor.
+      simplify. repeat split.
+
+      rewrite AssocMap.gcombine.
+      2: { reflexivity. }
+      rewrite AssocMap.gss.
+      unfold Verilog.merge_arr.
+      setoid_rewrite H1.
+      reflexivity.
+
+      rewrite combine_length.
+      unfold arr_repeat. simplify.
+      rewrite list_repeat_len.
+      reflexivity.
+
+      unfold arr_repeat. simplify.
+      rewrite list_repeat_len; auto.
+      intros.
+      erewrite array_get_error_equal.
+      eauto. apply combine_none.
+
+      assumption.
+
     - (* Iop *)
       (* destruct v eqn:?; *)
       (*          try ( *)
@@ -390,8 +469,195 @@ Section CORRECTNESS.
       (* assumption. *)
       admit.
 
-    - admit.
-    - admit.
+      Ltac rt :=
+        repeat match goal with
+        | [ _ : error _ _ = OK _ _ _ |- _ ] => discriminate
+        | [ _ : context[if (?x && ?y) then _ else _] |- _ ] =>
+          let EQ1 := fresh "EQ" in
+          let EQ2 := fresh "EQ" in
+          destruct x eqn:EQ1; destruct y eqn:EQ2; simpl in *
+        | [ _ : context[if ?x then _ else _] |- _ ] =>
+          let EQ := fresh "EQ" in
+          destruct x eqn:EQ; simpl in *
+        | [ H : ret _ _ = _  |- _ ] => invert H
+        | [ _ : context[match ?x with | _ => _ end] |- _ ] => destruct x
+        end.
+
+      Opaque Z.mul.
+
+    - (* FIXME: Should be able to use the spec to avoid destructing here. *)
+      destruct c, chunk, addr, args; simplify; rt; simplify.
+
+      + admit. (* FIXME: Alignment *)
+
+      + (* FIXME: Why is this degenerate? Should we support this mode? *)
+        unfold Op.eval_addressing in H0.
+        destruct (Archi.ptr64) eqn:ARCHI; simplify.
+        destruct (Registers.Regmap.get r0 rs) eqn:EQr0; discriminate.
+
+      + invert MARR. simplify.
+
+        unfold Op.eval_addressing in H0.
+        destruct (Archi.ptr64) eqn:ARCHI; simplify.
+
+        unfold reg_stack_based_pointers in RSBP.
+        pose proof (RSBP r0) as RSBPr0.
+        pose proof (RSBP r1) as RSBPr1.
+
+        destruct (Registers.Regmap.get r0 rs) eqn:EQr0;
+        destruct (Registers.Regmap.get r1 rs) eqn:EQr1; simplify.
+
+        rewrite ARCHI in H1. simplify.
+        subst.
+
+        eexists. split.
+        eapply Smallstep.plus_one.
+        eapply HTL.step_module; eauto.
+        econstructor. econstructor. econstructor. simplify.
+        econstructor. econstructor. econstructor. econstructor. simplify.
+        econstructor.
+        econstructor.
+        econstructor.
+        econstructor.
+        econstructor.
+        econstructor.
+        econstructor.
+        econstructor.
+        econstructor.
+        econstructor.
+        econstructor.
+        econstructor.
+        econstructor.
+        econstructor.
+        econstructor.
+        econstructor.
+        econstructor.
+        econstructor. (* FIXME: Oh dear. *)
+
+        unfold Verilog.arr_assocmap_lookup. simplify. setoid_rewrite H3.
+        f_equal.
+
+        simplify. unfold Verilog.merge_regs.
+        unfold_merge.
+        rewrite AssocMap.gso.
+        apply AssocMap.gss.
+        apply st_greater_than_res.
+
+        simplify. rewrite assumption_32bit.
+        econstructor; simplify; eauto.
+
+        unfold Verilog.merge_regs. unfold_merge.
+        apply regs_lessdef_add_match.
+
+        all: admit.
+
+      + invert MARR. simplify.
+
+        unfold Op.eval_addressing in H0.
+        destruct (Archi.ptr64) eqn:ARCHI; simplify.
+        rewrite ARCHI in H0. simplify.
+
+        (** Here we are assuming that any stack read will be within the bounds
+            of the activation record. *)
+        assert (0 <= Integers.Ptrofs.unsigned i0) as READ_BOUND_LOW by admit.
+        assert (Integers.Ptrofs.unsigned i0 < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit.
+
+        eexists. split.
+        eapply Smallstep.plus_one.
+        eapply HTL.step_module; eauto.
+        econstructor. econstructor. econstructor. simplify.
+        econstructor. econstructor. econstructor. econstructor. simplify.
+
+        unfold Verilog.arr_assocmap_lookup. setoid_rewrite H3.
+        f_equal.
+
+        simplify. unfold Verilog.merge_regs.
+        unfold_merge.
+        rewrite AssocMap.gso.
+        apply AssocMap.gss.
+        apply st_greater_than_res.
+
+        simplify. rewrite assumption_32bit.
+        econstructor; simplify; eauto.
+
+        unfold Verilog.merge_regs. unfold_merge.
+        apply regs_lessdef_add_match.
+
+        (** Equality proof *)
+        (* FIXME: 32-bit issue. *)
+        assert (forall x, valueToNat (ZToValue 32 x) = Z.to_nat x) as VALUE_IDENTITY by admit.
+        rewrite VALUE_IDENTITY.
+        specialize (H5 (Integers.Ptrofs.unsigned i0 / 4)).
+        rewrite Z2Nat.id in H5; try lia.
+        exploit H5; auto; intros.
+        1: {
+          split.
+          - apply Z.div_pos; lia.
+          - apply Zmult_lt_reg_r with (p := 4); try lia.
+            repeat rewrite ZLib.div_mul_undo; lia.
+        }
+        2: {
+          assert (0 < RTL.fn_stacksize f) by lia.
+          apply Z.div_pos; lia.
+        }
+        replace (4 * (Integers.Ptrofs.unsigned i0 / 4)) with (Integers.Ptrofs.unsigned i0) in H0.
+        2: {
+          rewrite Z.mul_comm.
+          rewrite ZLib.div_mul_undo; lia.
+        }
+        rewrite Integers.Ptrofs.repr_unsigned in H0.
+        rewrite H1 in H0.
+        invert H0. assumption.
+
+        apply regs_lessdef_add_greater.
+        apply greater_than_max_func.
+        assumption.
+
+        unfold state_st_wf. inversion 1. simplify.
+        unfold Verilog.merge_regs.
+        unfold_merge. rewrite AssocMap.gso.
+        apply AssocMap.gss.
+        apply st_greater_than_res.
+
+        econstructor.
+        repeat split; simplify.
+        unfold HTL.empty_stack.
+        simplify.
+        unfold Verilog.merge_arrs.
+
+        rewrite AssocMap.gcombine.
+        2: { reflexivity. }
+        rewrite AssocMap.gss.
+        unfold Verilog.merge_arr.
+        setoid_rewrite H3.
+        reflexivity.
+
+        rewrite combine_length.
+        unfold arr_repeat. simplify.
+        rewrite list_repeat_len.
+        reflexivity.
+
+        unfold arr_repeat. simplify.
+        rewrite list_repeat_len.
+        congruence.
+
+        intros.
+        erewrite array_get_error_equal.
+        eauto. apply combine_none.
+        assumption.
+
+        (* FIXME: RSBP Proof. *)
+
+    - destruct c, chunk, addr, args; simplify; rt; simplify.
+      + admit.
+      + admit.
+      + admit.
+
+      (* + eexists. split. *)
+      (*   eapply Smallstep.plus_one. *)
+      (*   eapply HTL.step_module; eauto. *)
+      (*   econstructor. econstructor. econstructor. simplify. *)
+      + admit.
 
     - eexists. split. apply Smallstep.plus_one.
       eapply HTL.step_module; eauto.
@@ -453,8 +719,7 @@ Section CORRECTNESS.
       econstructor; simpl; trivial.
       constructor.
 
-      constructor.
-      constructor.
+      constructor. constructor.
 
       unfold_merge. simpl.
       rewrite AssocMap.gso.
@@ -470,7 +735,8 @@ Section CORRECTNESS.
       apply AssocMap.gss.
       rewrite Events.E0_left. reflexivity.
       constructor.
-      assumption.
+
+      admit.
       constructor.
 
     - econstructor. split.
@@ -499,21 +765,38 @@ Section CORRECTNESS.
       apply AssocMap.gss.
       rewrite Events.E0_left. trivial.
 
-      constructor. assumption. simpl. inversion MASSOC. subst.
+      constructor.
+      admit.
+
+      simpl. inversion MASSOC. subst.
       unfold find_assocmap, AssocMapExt.get_default. rewrite AssocMap.gso.
       apply H1. eapply RTL.max_reg_function_use. eauto. simpl; tauto.
       apply st_greater_than_res.
 
     - inversion MSTATE; subst. inversion TF; subst.
       econstructor. split. apply Smallstep.plus_one.
-      eapply HTL.step_call.
+      eapply HTL.step_call. simpl.
 
       constructor. apply regs_lessdef_add_greater.
       apply greater_than_max_func.
       apply init_reg_assoc_empty. assumption. unfold state_st_wf.
       intros. inv H1. apply AssocMap.gss. constructor.
 
-      admit.
+      econstructor; simpl.
+      reflexivity.
+      rewrite AssocMap.gss. reflexivity.
+      intros.
+      destruct (Mem.load AST.Mint32 m' stk
+                         (Integers.Ptrofs.unsigned (Integers.Ptrofs.add
+                                                      Integers.Ptrofs.zero
+                                                      (Integers.Ptrofs.repr ptr)))) eqn:LOAD.
+      pose proof Mem.load_alloc_same as LOAD_ALLOC.
+      pose proof H as ALLOC.
+      eapply LOAD_ALLOC in ALLOC.
+      2: { exact LOAD. }
+      rewrite ALLOC.
+      repeat constructor.
+      constructor.
 
     - inversion MSTATE; subst. inversion MS; subst. econstructor.
       split. apply Smallstep.plus_one.
@@ -525,13 +808,11 @@ Section CORRECTNESS.
       unfold state_st_wf. intros. inv H. rewrite AssocMap.gso.
       rewrite AssocMap.gss. trivial. apply st_greater_than_res.
 
-      admit.
-
       Unshelve.
       exact (AssocMap.empty value).
       exact (AssocMap.empty value).
-      admit.
-      admit.
+      exact (AssocMap.empty value).
+      exact (AssocMap.empty value).
       (* exact (ZToValue 32 0). *)
       (* exact (AssocMap.empty value). *)
       (* exact (AssocMap.empty value). *)
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index b70e11c..d9c9912 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -163,11 +163,11 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt -
 | tr_instr_Iload :
     forall mem addr args s s' i c dst n,
       translate_arr_access mem addr args stk s = OK c s' i ->
-      tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n) (block dst c) (state_goto st n)
+      tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n) (nonblock dst c) (state_goto st n)
 | tr_instr_Istore :
     forall mem addr args s s' i c src n,
       translate_arr_access mem addr args stk s = OK c s' i ->
-      tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vblock c (Vvar src))
+      tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vnonblock c (Vvar src))
                (state_goto st n).
 Hint Constructors tr_instr : htlspec.
 
@@ -184,14 +184,16 @@ Hint Constructors tr_code : htlspec.
 
 Inductive tr_module (f : RTL.function) : module -> Prop :=
   tr_module_intro :
-    forall data control fin rtrn st stk m start rst clk scldecls arrdecls,
+    forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls,
       (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i ->
-                    tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) ->
+               tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) ->
+      stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) ->
+      Z.modulo (f.(RTL.fn_stacksize)) 4 = 0 ->
       m = (mkmodule f.(RTL.fn_params)
                         data
                         control
                         f.(RTL.fn_entrypoint)
-                        st stk fin rtrn start rst clk scldecls arrdecls) ->
+                        st stk stk_len fin rtrn start rst clk scldecls arrdecls) ->
       tr_module f m.
 Hint Constructors tr_module : htlspec.
 
@@ -432,6 +434,12 @@ Proof.
 Qed.
 Hint Resolve iter_expand_instr_spec : htlspec.
 
+Lemma create_arr_inv : forall w x y z a b c d,
+    create_arr w x y z = OK (a, b) c d -> y = b.
+Proof.
+  inversion 1. reflexivity.
+Qed.
+
 Theorem transl_module_correct :
   forall f m,
     transl_module f = Errors.OK m -> tr_module f m.
@@ -444,12 +452,17 @@ Proof.
   inversion s; subst.
 
   unfold transf_module in *.
-  monadInv Heqr.
+  destruct (Z.eq_dec (RTL.fn_stacksize f mod 4) 0); monadInv Heqr.
+
+  (* TODO: We should be able to fold this into the automation. *)
+  pose proof (create_arr_inv _ _ _ _ _ _ _ _ EQ0) as STK_LEN.
+  rewrite <- STK_LEN.
+
   econstructor; simpl; trivial.
   intros.
   inv_incr.
   assert (EQ3D := EQ3).
-  destruct x3.
+  destruct x4.
   apply collect_declare_datapath_trans in EQ3.
   apply collect_declare_controllogic_trans in EQ3D.
   assert (STC: st_controllogic s10 = st_controllogic s3) by congruence.
diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v
index efe3565..2b9974b 100644
--- a/src/translation/Veriloggen.v
+++ b/src/translation/Veriloggen.v
@@ -29,13 +29,13 @@ Fixpoint transl_list (st : list (node * Verilog.stmnt)) {struct st} : list (expr
 
 Fixpoint scl_to_Vdecl (scldecl : list (reg * (option io * scl_decl))) {struct scldecl} : list module_item :=
   match scldecl with
-  | (r, (io, Scalar sz))::scldecl' => Vdeclaration (Vdecl io r sz) :: scl_to_Vdecl scldecl'
+  | (r, (io, VScalar sz))::scldecl' => Vdeclaration (Vdecl io r sz) :: scl_to_Vdecl scldecl'
   | nil => nil
   end.
 
 Fixpoint arr_to_Vdeclarr (arrdecl : list (reg * (option io * arr_decl))) {struct arrdecl} : list module_item :=
   match arrdecl with
-  | (r, (io, Array sz l))::arrdecl' => Vdeclaration (Vdeclarr io r sz l) :: arr_to_Vdeclarr arrdecl'
+  | (r, (io, VArray sz l))::arrdecl' => Vdeclaration (Vdeclarr io r sz l) :: arr_to_Vdeclarr arrdecl'
   | nil => nil
   end.
 
@@ -56,6 +56,7 @@ Definition transl_module (m : HTL.module) : Verilog.module :=
                    m.(mod_return)
                    m.(mod_st)
                    m.(mod_stk)
+                   m.(mod_stk_len)
                    m.(mod_params)
                    body
                    m.(mod_entrypoint).
diff --git a/src/verilog/Array.v b/src/verilog/Array.v
new file mode 100644
index 0000000..fc52f04
--- /dev/null
+++ b/src/verilog/Array.v
@@ -0,0 +1,271 @@
+Set Implicit Arguments.
+
+Require Import Lia.
+Require Import Coquplib.
+From Coq Require Import Lists.List Datatypes.
+
+Import ListNotations.
+
+Local Open Scope nat_scope.
+
+Record Array (A : Type) : Type :=
+  mk_array
+    { arr_contents : list A
+    ; arr_length : nat
+    ; arr_wf : length arr_contents = arr_length
+    }.
+
+Definition make_array {A : Type} (l : list A) : Array A :=
+  @mk_array A l (length l) eq_refl.
+
+Fixpoint list_set {A : Type} (i : nat) (x : A) (l : list A) {struct l} : list A :=
+  match i, l with
+  | _, nil => nil
+  | S n, h :: t => h :: list_set n x t
+  | O, h :: t => x :: t
+  end.
+
+Lemma list_set_spec1 {A : Type} :
+  forall l i (x : A),
+    i < length l -> nth_error (list_set i x l) i = Some x.
+Proof.
+  induction l; intros; destruct i; simplify; try lia; try reflexivity; firstorder.
+Qed.
+Hint Resolve list_set_spec1 : array.
+
+Lemma list_set_spec2 {A : Type} :
+  forall l i (x : A) d,
+    i < length l -> nth i (list_set i x l) d = x.
+Proof.
+  induction l; intros; destruct i; simplify; try lia; try reflexivity; firstorder.
+Qed.
+Hint Resolve list_set_spec2 : array.
+
+Lemma array_set_wf {A : Type} :
+  forall l ln i (x : A),
+    length l = ln -> length (list_set i x l) = ln.
+Proof.
+  induction l; intros; destruct i; auto.
+
+  invert H; simplify; auto.
+Qed.
+
+Definition array_set {A : Type} (i : nat) (x : A) (a : Array A) :=
+  let l := a.(arr_contents) in
+  let ln := a.(arr_length) in
+  let WF := a.(arr_wf) in
+  @mk_array A (list_set i x l) ln (@array_set_wf A l ln i x WF).
+
+Lemma array_set_spec1 {A : Type} :
+  forall a i (x : A),
+    i < a.(arr_length) -> nth_error ((array_set i x a).(arr_contents)) i = Some x.
+Proof.
+  intros.
+
+  rewrite <- a.(arr_wf) in H.
+  unfold array_set. simplify.
+  eauto with array.
+Qed.
+Hint Resolve array_set_spec1 : array.
+
+Lemma array_set_spec2 {A : Type} :
+  forall a i (x : A) d,
+    i < a.(arr_length) -> nth i ((array_set i x a).(arr_contents)) d = x.
+Proof.
+  intros.
+
+  rewrite <- a.(arr_wf) in H.
+  unfold array_set. simplify.
+  eauto with array.
+Qed.
+Hint Resolve array_set_spec2 : array.
+
+Definition array_get_error {A : Type} (i : nat) (a : Array A) : option A :=
+  nth_error a.(arr_contents) i.
+
+Lemma array_get_error_equal {A : Type} :
+  forall (a b : Array A) i,
+    a.(arr_contents) = b.(arr_contents) ->
+    array_get_error i a = array_get_error i b.
+Proof.
+  unfold array_get_error. congruence.
+Qed.
+
+Lemma array_get_error_bound {A : Type} :
+  forall (a : Array A) i,
+    i < a.(arr_length) -> exists x, array_get_error i a = Some x.
+Proof.
+  intros.
+
+  rewrite <- a.(arr_wf) in H.
+  assert (~ length (arr_contents a) <= i) by lia.
+
+  pose proof (nth_error_None a.(arr_contents) i).
+  apply not_iff_compat in H1.
+  apply <- H1 in H0.
+
+  destruct (nth_error (arr_contents a) i) eqn:EQ; try contradiction; eauto.
+Qed.
+
+Lemma array_get_error_set_bound {A : Type} :
+  forall (a : Array A) i x,
+    i < a.(arr_length) -> array_get_error i (array_set i x a) = Some x.
+Proof.
+  intros.
+
+  unfold array_get_error.
+  eauto with array.
+Qed.
+
+Definition array_get {A : Type} (i : nat) (x : A) (a : Array A) : A :=
+  nth i a.(arr_contents) x.
+
+Lemma array_get_set_bound {A : Type} :
+  forall (a : Array A) i x d,
+    i < a.(arr_length) -> array_get i d (array_set i x a) = x.
+Proof.
+  intros.
+
+  unfold array_get.
+  info_eauto with array.
+Qed.
+
+(** Tail recursive version of standard library function. *)
+Fixpoint list_repeat' {A : Type} (acc : list A) (a : A) (n : nat) : list A :=
+  match n with
+  | O => acc
+  | S n => list_repeat' (a::acc) a n
+  end.
+
+Lemma list_repeat'_len {A : Type} : forall (a : A) n l,
+    length (list_repeat' l a n) = (n + Datatypes.length l)%nat.
+Proof.
+  induction n; intros; simplify; try reflexivity.
+
+  specialize (IHn (a :: l)).
+  rewrite IHn.
+  simplify.
+  lia.
+Qed.
+
+Lemma list_repeat'_app {A : Type} : forall (a : A) n l,
+    list_repeat' l a n = list_repeat' [] a n ++ l.
+Proof.
+  induction n; intros; simplify; try reflexivity.
+
+  pose proof IHn.
+  specialize (H (a :: l)).
+  rewrite H. clear H.
+  specialize (IHn (a :: nil)).
+  rewrite IHn. clear IHn.
+  remember (list_repeat' [] a n) as l0.
+
+  rewrite <- app_assoc.
+  f_equal.
+Qed.
+
+Lemma list_repeat'_head_tail {A : Type} : forall n (a : A),
+  a :: list_repeat' [] a n = list_repeat' [] a n ++ [a].
+Proof.
+  induction n; intros; simplify; try reflexivity.
+  rewrite list_repeat'_app.
+
+  replace (a :: list_repeat' [] a n ++ [a]) with (list_repeat' [] a n ++ [a] ++ [a]).
+  2: { rewrite app_comm_cons. rewrite IHn; auto.
+       rewrite app_assoc. reflexivity. }
+  rewrite app_assoc. reflexivity.
+Qed.
+
+Lemma list_repeat'_cons {A : Type} : forall (a : A) n,
+    list_repeat' [a] a n = a :: list_repeat' [] a n.
+Proof.
+  intros.
+
+  rewrite list_repeat'_head_tail; auto.
+  apply list_repeat'_app.
+Qed.
+
+Definition list_repeat {A : Type} : A -> nat -> list A := list_repeat' nil.
+
+Lemma list_repeat_len {A : Type} : forall n (a : A), length (list_repeat a n) = n.
+Proof.
+  intros.
+  unfold list_repeat.
+  rewrite list_repeat'_len.
+  simplify. lia.
+Qed.
+
+Lemma dec_list_repeat_spec {A : Type} : forall n (a : A) a',
+    (forall x x' : A, {x' = x} + {~ x' = x}) ->
+    In a' (list_repeat a n) -> a' = a.
+Proof.
+  induction n; intros; simplify; try contradiction.
+
+  unfold list_repeat in *.
+  simplify.
+
+  rewrite list_repeat'_app in H.
+  pose proof (X a a').
+  destruct H0; auto.
+
+  (* This is actually a degenerate case, not an unprovable goal. *)
+  pose proof (in_app_or (list_repeat' [] a n) ([a])).
+  apply H0 in H. invert H.
+
+  - eapply IHn in X; eassumption.
+  - invert H1; contradiction.
+Qed.
+
+Lemma list_repeat_head_tail {A : Type} : forall n (a : A),
+    a :: list_repeat a n = list_repeat a n ++ [a].
+Proof.
+  unfold list_repeat. apply list_repeat'_head_tail.
+Qed.
+
+Lemma list_repeat_cons {A : Type} : forall n (a : A),
+    list_repeat a (S n) = a :: list_repeat a n.
+Proof.
+  intros.
+
+  unfold list_repeat.
+  apply list_repeat'_cons.
+Qed.
+
+Definition arr_repeat {A : Type} (a : A) (n : nat) : Array A := make_array (list_repeat a n).
+
+Fixpoint list_combine {A B C : Type} (f : A -> B -> C) (x : list A) (y : list B) : list C :=
+  match x, y with
+  | a :: t, b :: t' => f a b :: list_combine f t t'
+  | _, _ => nil
+  end.
+
+Lemma list_combine_length {A B C : Type} (f : A -> B -> C) : forall (x : list A) (y : list B),
+    length (list_combine f x y) = min (length x) (length y).
+Proof.
+  induction x; intros; simplify; try reflexivity.
+
+  destruct y; simplify; auto.
+Qed.
+
+Definition combine {A B C : Type} (f : A -> B -> C) (x : Array A) (y : Array B) : Array C :=
+  make_array (list_combine f x.(arr_contents) y.(arr_contents)).
+
+Lemma combine_length {A B C: Type} : forall x y (f : A -> B -> C),
+    x.(arr_length) = y.(arr_length) -> arr_length (combine f x y) = x.(arr_length).
+Proof.
+  intros.
+
+  unfold combine.
+  unfold make_array.
+  simplify.
+
+  rewrite <- (arr_wf x) in *.
+  rewrite <- (arr_wf y) in *.
+
+  destruct (arr_contents x); simplify.
+  - reflexivity.
+  - destruct (arr_contents y); simplify.
+    f_equal.
+    rewrite list_combine_length.
+    destruct (Min.min_dec (length l) (length l0)); congruence.
+Qed.
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
index c07d672..0bf5072 100644
--- a/src/verilog/HTL.v
+++ b/src/verilog/HTL.v
@@ -17,7 +17,7 @@
  *)
 
 From Coq Require Import FSets.FMapPositive.
-From coqup Require Import Coquplib Value AssocMap.
+From coqup Require Import Coquplib Value AssocMap Array.
 From coqup Require Verilog.
 From compcert Require Events Globalenvs Smallstep Integers Values.
 From compcert Require Import Maps.
@@ -46,6 +46,7 @@ Record module: Type :=
     mod_entrypoint : node;
     mod_st : reg;
     mod_stk : reg;
+    mod_stk_len : nat;
     mod_finish : reg;
     mod_return : reg;
     mod_start : reg;
@@ -65,6 +66,9 @@ Fixpoint init_regs (vl : list value) (rl : list reg) {struct rl} :=
   | _, _ => empty_assocmap
   end.
 
+Definition empty_stack (m : module) : Verilog.assocmap_arr :=
+  (AssocMap.set m.(mod_stk) (Array.arr_repeat None m.(mod_stk_len)) (AssocMap.empty Verilog.arr)).
+
 (** * Operational Semantics *)
 
 Definition genv := Globalenvs.Genv.t fundef unit.
@@ -74,7 +78,8 @@ Inductive stackframe : Type :=
     forall  (res : reg)
             (m : module)
             (pc : node)
-            (assoc : assocmap),
+            (reg_assoc : Verilog.assocmap_reg)
+            (arr_assoc : Verilog.assocmap_arr),
       stackframe.
 
 Inductive state : Type :=
@@ -82,8 +87,8 @@ Inductive state : Type :=
     forall (stack : list stackframe)
            (m : module)
            (st : node)
-           (reg_assoc : assocmap)
-           (arr_assoc : AssocMap.t (list value)), state
+           (reg_assoc : Verilog.assocmap_reg)
+           (arr_assoc : Verilog.assocmap_arr), state
 | Returnstate :
     forall (res : list stackframe)
            (v : value), state
@@ -104,7 +109,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
       m.(mod_datapath)!st = Some data ->
       Verilog.stmnt_runp f
         (Verilog.mkassociations asr empty_assocmap)
-        (Verilog.mkassociations asa (AssocMap.empty (list value)))
+        (Verilog.mkassociations asa (empty_stack m))
         ctrl
         (Verilog.mkassociations basr1 nasr1)
         (Verilog.mkassociations basa1 nasa1) ->
@@ -114,8 +119,8 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
         data
         (Verilog.mkassociations basr2 nasr2)
         (Verilog.mkassociations basa2 nasa2) ->
-      asr' = merge_assocmap nasr2 basr2 ->
-      asa' = AssocMapExt.merge (list value) nasa2 basa2 ->
+      asr' = Verilog.merge_regs nasr2 basr2 ->
+      asa' = Verilog.merge_arrs nasa2 basa2 ->
       asr'!(m.(mod_st)) = Some stval ->
       valueToPos stval = pstval ->
       step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa')
@@ -130,13 +135,12 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
            (State res m m.(mod_entrypoint)
              (AssocMap.set (mod_st m) (posToValue 32 m.(mod_entrypoint))
                            (init_regs args m.(mod_params)))
-              (AssocMap.empty (list value)))
+             (empty_stack m))
 | step_return :
-    forall g m asr i r sf pc mst,
+    forall g m asr asa i r sf pc mst,
       mst = mod_st m ->
-      step g (Returnstate (Stackframe r m pc asr :: sf) i) Events.E0
-           (State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i)
-                  (AssocMap.empty (list value))).
+      step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0
+           (State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i) asa).
 Hint Constructors step : htl.
 
 Inductive initial_state (p: program): state -> Prop :=
diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index d527b15..b1ee353 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -296,6 +296,11 @@ Inductive val_value_lessdef: val -> value -> Prop :=
     val_value_lessdef (Vint i) 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 n z,
   (- Z.of_nat (2 ^ n) <= z < Z.of_nat (2 ^ n))%Z ->
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index b80678e..7d5e3c0 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -25,9 +25,11 @@ From Coq Require Import
   Lists.List
   Program.
 
+Require Import Lia.
+
 Import ListNotations.
 
-From coqup Require Import common.Coquplib common.Show verilog.Value AssocMap.
+From coqup Require Import common.Coquplib common.Show verilog.Value AssocMap Array.
 From compcert Require Integers Events.
 From compcert Require Import Errors Smallstep Globalenvs.
 
@@ -47,39 +49,51 @@ Record associations (A : Type) : Type :=
     assoc_nonblocking : AssocMap.t A
   }.
 
+Definition arr := (Array (option value)).
+
 Definition reg_associations := associations value.
-Definition arr_associations := associations (list value).
+Definition arr_associations := associations arr.
 
-Definition assocmap_arr := AssocMap.t (list value).
+Definition assocmap_reg := AssocMap.t value.
+Definition assocmap_arr := AssocMap.t arr.
 
-Definition merge_associations {A : Type} (assoc : associations A) :=
-  mkassociations (AssocMapExt.merge A assoc.(assoc_nonblocking) assoc.(assoc_blocking))
-                 (AssocMap.empty A).
+Definition merge_regs (new : assocmap_reg) (old : assocmap_reg) : assocmap_reg :=
+  AssocMapExt.merge value new old.
+
+Definition merge_cell (new : option value) (old : option value) : option value :=
+  match new, old with
+  | Some _, _ => new
+  | _, _ => old
+  end.
+
+Definition merge_arr (new : option arr) (old : option arr) : option arr :=
+  match new, old with
+  | Some new', Some old' => Some (combine merge_cell new' old')
+  | Some new', None => Some new'
+  | None, Some old' => Some old'
+  | None, None => None
+  end.
+
+Definition merge_arrs (new : assocmap_arr) (old : assocmap_arr) : assocmap_arr :=
+  AssocMap.combine merge_arr new old.
 
 Definition arr_assocmap_lookup (a : assocmap_arr) (r : reg) (i : nat) : option value :=
   match a ! r with
   | None => None
-  | Some arr => nth_error arr i
-  end.
-
-Fixpoint list_set {A : Type} (i : nat) (x : A) (l : list A) : list A :=
-  match i, l with
-  | _, nil => nil
-  | S n, h :: t => h :: list_set n x t
-  | O, h :: t => x :: t
+  | Some arr => Some (Option.default (NToValue 32 0) (Option.join (array_get_error i arr)))
   end.
 
-Definition assocmap_l_set (r : reg) (i : nat) (v : value) (a : assocmap_arr) : assocmap_arr :=
+Definition arr_assocmap_set (r : reg) (i : nat) (v : value) (a : assocmap_arr) : assocmap_arr :=
   match a ! r with
   | None => a
-  | Some arr => AssocMap.set r (list_set i v arr) a
+  | Some arr => a # r <- (array_set i (Some v) arr)
   end.
 
 Definition block_arr (r : reg) (i : nat) (asa : arr_associations) (v : value) : arr_associations :=
-  mkassociations (assocmap_l_set r i v asa.(assoc_blocking)) asa.(assoc_nonblocking).
+  mkassociations (arr_assocmap_set r i v asa.(assoc_blocking)) asa.(assoc_nonblocking).
 
 Definition nonblock_arr (r : reg) (i : nat) (asa : arr_associations) (v : value) : arr_associations :=
-  mkassociations asa.(assoc_blocking) (assocmap_l_set r i v asa.(assoc_nonblocking)).
+  mkassociations asa.(assoc_blocking) (arr_assocmap_set r i v asa.(assoc_nonblocking)).
 
 Definition block_reg (r : reg) (asr : reg_associations) (v : value) :=
   mkassociations (AssocMap.set r v asr.(assoc_blocking)) asr.(assoc_nonblocking).
@@ -87,8 +101,8 @@ Definition block_reg (r : reg) (asr : reg_associations) (v : value) :=
 Definition nonblock_reg (r : reg) (asr : reg_associations) (v : value) :=
   mkassociations asr.(assoc_blocking) (AssocMap.set r v asr.(assoc_nonblocking)).
 
-Inductive scl_decl : Type := Scalar (sz : nat).
-Inductive arr_decl : Type := Array (sz : nat) (ln : nat).
+Inductive scl_decl : Type := VScalar (sz : nat).
+Inductive arr_decl : Type := VArray (sz : nat) (ln : nat).
 
 (** * Verilog AST
 
@@ -218,6 +232,7 @@ Record module : Type := mkmodule {
   mod_return : reg;
   mod_st : reg; (**r Variable that defines the current state, it should be internal. *)
   mod_stk : reg;
+  mod_stk_len : nat;
   mod_args : list reg;
   mod_body : list module_item;
   mod_entrypoint : node;
@@ -235,7 +250,7 @@ Definition posToLit (p : positive) : expr :=
 Coercion Vlit : value >-> expr.
 Coercion Vvar : reg >-> expr.
 
-Definition fext := AssocMap.t value.
+Definition fext := assocmap.
 Definition fextclk := nat -> fext.
 
 (** ** State
@@ -272,8 +287,8 @@ Inductive state : Type :=
     forall (stack : list stackframe)
            (m : module)
            (st : node)
-           (reg_assoc : assocmap)
-           (arr_assoc : AssocMap.t (list value)), state
+           (reg_assoc : assocmap_reg)
+           (arr_assoc : assocmap_arr), state
 | Returnstate :
     forall (res : list stackframe)
            (v : value), state
@@ -691,17 +706,19 @@ Fixpoint init_params (vl : list value) (rl : list reg) {struct rl} :=
   end.
 
 Definition genv := Globalenvs.Genv.t fundef unit.
+Definition empty_stack (m : module) : assocmap_arr :=
+  (AssocMap.set m.(mod_stk) (Array.arr_repeat None m.(mod_stk_len)) (AssocMap.empty arr)).
 
 Inductive step : genv -> state -> Events.trace -> state -> Prop :=
   | step_module :
       forall asr asa asr' asa' basr1 nasr1 basa1 nasa1 f stval pstval m sf st g,
       mis_stepp f (mkassociations asr empty_assocmap)
-                  (mkassociations asa (AssocMap.empty (list value)))
+                  (mkassociations asa (empty_stack m))
                   m.(mod_body)
                   (mkassociations basr1 nasr1)
                   (mkassociations basa1 nasa1)->
-      asr' = merge_assocmap nasr1 basr1 ->
-      asa' = AssocMapExt.merge (list value) nasa1 basa1 ->
+      asr' = merge_regs nasr1 basr1 ->
+      asa' = merge_arrs nasa1 basa1 ->
       asr'!(m.(mod_st)) = Some stval ->
       valueToPos stval = pstval ->
       step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa')
@@ -716,13 +733,13 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
          (State res m m.(mod_entrypoint)
           (AssocMap.set m.(mod_st) (posToValue 32 m.(mod_entrypoint))
            (init_params args m.(mod_args)))
-          (AssocMap.empty (list value)))
+          (empty_stack m))
 | step_return :
     forall g m asr i r sf pc mst,
     mst = mod_st m ->
     step g (Returnstate (Stackframe r m pc asr :: sf) i) Events.E0
          (State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i)
-                (AssocMap.empty (list value))).
+                (empty_stack m)).
 Hint Constructors step : verilog.
 
 Inductive initial_state (p: program): state -> Prop :=