Merge pull request #5 from p0llard/arrays-proof

Array/memory functionality

7 files changed, 643 insertions, 351 deletions

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 78b1864..b573b06 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -27,10 +27,15 @@ Hint Resolve AssocMap.gss : htlh.
 Hint Resolve Ple_refl : htlh.
 Hint Resolve Ple_succ : htlh.
 
+Inductive scl_decl : Type := Scalar (sz : nat).
+Inductive arr_decl : Type := Array (sz : nat) (ln : nat).
+
 Record state: Type := mkstate {
   st_st : reg;
   st_freshreg: reg;
   st_freshstate: node;
+  st_scldecls: AssocMap.t scl_decl;
+  st_arrdecls: AssocMap.t arr_decl;
   st_datapath: datapath;
   st_controllogic: controllogic;
 }.
@@ -39,6 +44,8 @@ Definition init_state (st : reg) : state :=
   mkstate st
           1%positive
           1%positive
+          (AssocMap.empty scl_decl)
+          (AssocMap.empty arr_decl)
           (AssocMap.empty stmnt)
           (AssocMap.empty stmnt).
 
@@ -68,19 +75,9 @@ Module HTLState <: State.
   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.
-    - rewrite H1. rewrite H. reflexivity.
-    - intros. destruct H4 with n.
-      + left; assumption.
-      + destruct H8 with n;
-          [ rewrite <- H0; left; assumption
-          | right; rewrite <- H0; apply H10
-          ].
-    - intros. destruct H5 with n.
-      + left; assumption.
-      + destruct H9 with n.
-        * rewrite <- H0. left. assumption.
-        * right. rewrite <- H0. apply H10.
+    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.
@@ -102,13 +99,13 @@ Definition state_cond (st : reg) (c : expr) (n1 n2 : node) : stmnt :=
 Definition check_empty_node_datapath:
   forall (s: state) (n: node), { s.(st_datapath)!n = None } + { True }.
 Proof.
-  intros. case (s.(st_datapath)!n); intros. right; auto. left; auto.
+  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); intros. right; auto. left; auto.
+  intros. case (s.(st_controllogic)!n); tauto.
 Defined.
 
 Lemma add_instr_state_incr :
@@ -120,6 +117,8 @@ Lemma add_instr_state_incr :
        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.
@@ -136,6 +135,8 @@ Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit :=
                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)
@@ -151,6 +152,8 @@ Lemma add_instr_skip_state_incr :
        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.
@@ -167,6 +170,8 @@ Definition add_instr_skip (n : node) (st : stmnt) : mon unit :=
                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)
@@ -224,9 +229,14 @@ Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon ex
   | Op.Aindexed off, r1::nil => ret (boplitz Vadd r1 off)
   | Op.Aindexed2 off, r1::r2::nil => ret (Vbinop Vadd (Vvar r1) (boplitz Vadd r2 off))
   | Op.Ascaled scale offset, r1::nil =>
-    ret (Vbinop Vadd (boplitz Vadd r1 scale) (Vlit (ZToValue 32%nat offset)))
+    ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue 32 offset)))
   | Op.Aindexed2scaled scale offset, r1::r2::nil =>
     ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale))
+  (* Stack arrays/referenced variables *)
+  | 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 (Vlit (ZToValue 32 (a / 4)))
+    else error (Errors.msg "Veriloggen: eff_addressing misaligned stack offset")
   | _, _ => error (Errors.msg "Veriloggen: eff_addressing instruction not implemented: other")
   end.
 
@@ -263,6 +273,8 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr :=
   | Op.Oshldimm n, r::nil => error (Errors.msg "Veriloggen: Instruction not implemented: Oshldimm")
   | Op.Ocmp c, _ => translate_condition c args
   | Op.Olea a, _ => translate_eff_addressing a args
+  | Op.Oleal a, _ => translate_eff_addressing a args (* FIXME: Need to be careful here; large arrays might fail? *)
+  | Op.Ocast32signed, r::nil => ret (Vvar r) (* FIXME: Don't need to sign extend for now since everything is 32 bit? *)
   | _, _ => error (Errors.msg "Veriloggen: Instruction not implemented: other")
   end.
 
@@ -274,6 +286,8 @@ Lemma add_branch_instr_state_incr:
                  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.
@@ -290,13 +304,34 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit :=
                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 "Veriloggen: add_branch_instr")
     end.
 
-Definition transf_instr (fin rtrn: reg) (ni: node * instruction) : 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 => ret (Vvari stack (boplitz Vadd r1 off)) (* FIXME: Cannot guarantee alignment *)
+  | 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 "Veriloggen: translate_arr_access address misaligned")
+  | 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 (boplitz Vadd r1 (offset / 4)) (boplitz Vmul r2 (scale / 4))))
+    else error (Errors.msg "Veriloggen: translate_arr_access address misaligned")
+  | 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 "Veriloggen: eff_addressing misaligned stack offset")
+  | _, _ => error (Errors.msg "Veriloggen: translate_arr_access unsuported addressing")
+  end.
+
+Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit :=
   match ni with
     (n, i) =>
     match i with
@@ -304,8 +339,12 @@ Definition transf_instr (fin rtrn: reg) (ni: node * instruction) : mon unit :=
     | Iop op args dst n' =>
       do instr <- translate_instr op args;
       add_instr n n' (nonblock dst instr)
-    | Iload _ _ _ _ _ => error (Errors.msg "Loads are not implemented.")
-    | Istore _ _ _ _ _ => error (Errors.msg "Stores are not implemented.")
+    | Iload mem addr args dst n' =>
+      do src <- translate_arr_access mem addr args stack;
+      add_instr n n' (block 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. *)
     | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.")
     | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.")
     | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.")
@@ -324,32 +363,61 @@ Definition transf_instr (fin rtrn: reg) (ni: node * instruction) : mon unit :=
   end.
 
 Lemma create_reg_state_incr:
-  forall s,
+  forall s sz,
+    st_incr s (mkstate
+         s.(st_st)
+         (Pos.succ (st_freshreg s))
+         (st_freshstate s)
+         (AssocMap.set s.(st_freshreg) (Scalar sz) s.(st_scldecls))
+         s.(st_arrdecls)
+         (st_datapath s)
+         (st_controllogic s)).
+Proof. constructor; simpl; auto with htlh. Qed.
+
+Definition create_reg (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) (Scalar sz) s.(st_scldecls))
+                   (st_arrdecls s)
+                   (st_datapath s)
+                   (st_controllogic s))
+              (create_reg_state_incr s sz).
+
+Lemma create_arr_state_incr:
+  forall s sz ln,
     st_incr s (mkstate
          s.(st_st)
          (Pos.succ (st_freshreg s))
          (st_freshstate s)
+         s.(st_scldecls)
+         (AssocMap.set s.(st_freshreg) (Array sz ln) s.(st_arrdecls))
          (st_datapath s)
          (st_controllogic s)).
 Proof. constructor; simpl; auto with htlh. Qed.
 
-Definition create_reg: mon reg :=
+Definition create_arr (sz : nat) (ln : nat) : mon reg :=
   fun s => let r := s.(st_freshreg) in
            OK r (mkstate
                    s.(st_st)
                    (Pos.succ r)
                    (st_freshstate s)
+                   s.(st_scldecls)
+                   (AssocMap.set s.(st_freshreg) (Array sz ln) s.(st_arrdecls))
                    (st_datapath s)
                    (st_controllogic s))
-              (create_reg_state_incr s).
+              (create_arr_state_incr s sz ln).
 
 Definition transf_module (f: function) : mon module :=
-  do fin <- create_reg;
-  do rtrn <- create_reg;
-  do _ <- collectlist (transf_instr fin rtrn) (Maps.PTree.elements f.(RTL.fn_code));
-  do start <- create_reg;
-  do rst <- create_reg;
-  do clk <- create_reg;
+  do fin <- create_reg 1;
+  do rtrn <- create_reg 32;
+  do stack <- create_arr 32 (Z.to_nat (f.(fn_stacksize) / 4));
+  do _ <- collectlist (transf_instr fin rtrn stack) (Maps.PTree.elements f.(RTL.fn_code));
+  do start <- create_reg 1;
+  do rst <- create_reg 1;
+  do clk <- create_reg 1;
   do current_state <- get;
   ret (mkmodule
          f.(RTL.fn_params)
@@ -357,6 +425,7 @@ Definition transf_module (f: function) : mon module :=
          current_state.(st_controllogic)
          f.(fn_entrypoint)
          current_state.(st_st)
+         stack
          fin
          rtrn).
 
@@ -365,6 +434,8 @@ Definition max_state (f: function) : state :=
   mkstate st
           (Pos.succ st)
           (Pos.succ (max_pc_function f))
+          (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 204451c..523c86c 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -16,8 +16,8 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From compcert Require RTL Registers AST.
-From compcert Require Import Globalenvs.
+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 HTL Verilog.
 
@@ -37,9 +37,9 @@ Inductive match_assocmaps : RTL.function -> RTL.regset -> assocmap -> Prop :=
 Hint Constructors match_assocmaps : htlproof.
 
 Definition state_st_wf (m : HTL.module) (s : HTL.state) :=
-  forall st assoc res,
-  s = HTL.State res m st assoc ->
-  assoc!(m.(HTL.mod_st)) = Some (posToValue 32 st).
+  forall st asa asr res,
+  s = HTL.State res m st asa asr ->
+  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 :=
@@ -53,14 +53,27 @@ Inductive match_stacks : list RTL.stackframe -> list HTL.stackframe -> Prop :=
       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.
+
 Inductive match_states : RTL.state -> HTL.state -> Prop :=
-| match_state : forall assoc sf f sp rs mem m st res
-    (MASSOC : match_assocmaps f rs assoc)
+| match_state : forall asa asr sf f 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 assoc))
-    (MS : match_stacks sf res),
+    (WF : state_st_wf m (HTL.State res m st asr asa))
+    (MS : match_stacks sf res)
+    (MA : match_arrs m f mem asa),
     match_states (RTL.State sf f sp st rs mem)
-                 (HTL.State res m st assoc)
+                 (HTL.State res m st asr asa)
 | match_returnstate :
     forall
       v v' stack m res
@@ -151,7 +164,7 @@ Ltac inv_state :=
       inversion TF;
       match goal with
         TC : forall _ _,
-          Maps.PTree.get _ _ = Some _ -> tr_code _ _ _ _ _ _ _ _,
+          Maps.PTree.get _ _ = Some _ -> tr_code _ _ _ _ _ _ _ _ _,
         H : Maps.PTree.get _ _ = Some _ |- _ =>
         apply TC in H; inversion H;
         match goal with
@@ -227,22 +240,22 @@ Section CORRECTNESS.
   Hint Resolve senv_preserved : htlproof.
 
   Lemma eval_correct :
-    forall sp op rs args m v v' e assoc f,
+    forall sp op rs args m v v' e asr asa f,
       Op.eval_operation ge sp op
 (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some v ->
       tr_op op args e ->
       val_value_lessdef v v' ->
-      Verilog.expr_runp f assoc e v'.
+      Verilog.expr_runp f asr asa e v'.
   Admitted.
 
   Lemma eval_cond_correct :
-    forall cond (args : list Registers.reg) s1 c s' i rs args m b f assoc,
+    forall cond (args : list Registers.reg) s1 c s' i rs args m b f asr asa,
     translate_condition cond args s1 = OK c s' i ->
     Op.eval_condition
       cond
       (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args)
       m = Some b ->
-    Verilog.expr_runp f assoc c (boolToValue 32 b).
+    Verilog.expr_runp f asr asa c (boolToValue 32 b).
   Admitted.
 
   (** The proof of semantic preservation for the translation of instructions
@@ -263,10 +276,10 @@ Section CORRECTNESS.
    *)
 
   Definition transl_instr_prop (instr : RTL.instruction) : Prop :=
-    forall m assoc fin rtrn st stmt trans res,
-      tr_instr fin rtrn st instr stmt trans ->
-      exists assoc',
-        HTL.step tge (HTL.State res m st assoc) Events.E0 (HTL.State res m st assoc').
+    forall m asr asa fin rtrn st stmt trans res,
+      tr_instr fin rtrn st (m.(HTL.mod_stk)) instr stmt trans ->
+      exists asr' asa',
+        HTL.step tge (HTL.State res m st asr asa) Events.E0 (HTL.State res m st asr' asa').
 
   Theorem transl_step_correct:
     forall (S1 : RTL.state) t S2,
@@ -285,10 +298,12 @@ Section CORRECTNESS.
       (* processing of state *)
       econstructor.
       simpl. trivial.
-      econstructor. trivial.
+      econstructor.
+      econstructor.
       econstructor.
 
       (* prove stval *)
+      unfold merge_assocmap.
       unfold_merge. simpl. apply AssocMap.gss.
 
       (* prove match_state *)
@@ -298,87 +313,94 @@ Section CORRECTNESS.
       assumption.
       unfold state_st_wf. inversion 1. subst. unfold_merge. apply AssocMap.gss.
     - (* Iop *)
-      destruct v eqn:?;
-               try (
-                 destruct op eqn:?; inversion H21; simpl in H0; repeat (unfold_match H0);
-                 inversion H0; subst; simpl in *; try (unfold_func H4); try (unfold_func H5);
-                 try (unfold_func H6);
-                 try (unfold Op.eval_addressing32 in H6; repeat (unfold_match H6); inversion H6;
-                      unfold_func H3);
-
-                 inversion Heql; inversion MASSOC; subst;
-                 assert (HPle : Ple r (RTL.max_reg_function f))
-                   by (eapply RTL.max_reg_function_use; eauto; simpl; auto);
-                 apply H1 in HPle; inversion HPle;
-                 rewrite H2 in *; discriminate
-               ).
-
-      + econstructor. split.
-      apply Smallstep.plus_one.
-      eapply HTL.step_module; eauto.
-      econstructor; simpl; trivial.
-      constructor; trivial.
-      econstructor; simpl; eauto.
-      eapply eval_correct; eauto. constructor.
-      unfold_merge. simpl.
-      rewrite AssocMap.gso.
-      apply AssocMap.gss.
-      apply st_greater_than_res.
-
-      (* match_states *)
-      assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit.
-      rewrite <- H1.
-      constructor; auto.
-      unfold_merge.
-      apply regs_lessdef_add_match.
-      constructor.
-      apply regs_lessdef_add_greater.
-      apply greater_than_max_func.
-      assumption.
-
-      unfold state_st_wf. intros. inversion H2. subst.
-      unfold_merge.
-      rewrite AssocMap.gso.
-      apply AssocMap.gss.
-      apply st_greater_than_res.
-
-      + econstructor. split.
-      apply Smallstep.plus_one.
+      (* destruct v eqn:?; *)
+      (*          try ( *)
+      (*            destruct op eqn:?; inversion H21; simpl in H0; repeat (unfold_match H0); *)
+      (*            inversion H0; subst; simpl in *; try (unfold_func H4); try (unfold_func H5); *)
+      (*            try (unfold_func H6); *)
+      (*            try (unfold Op.eval_addressing32 in H6; repeat (unfold_match H6); inversion H6; *)
+      (*                 unfold_func H3); *)
+
+      (*            inversion Heql; inversion MASSOC; subst; *)
+      (*            assert (HPle : Ple r (RTL.max_reg_function f)) *)
+      (*              by (eapply RTL.max_reg_function_use; eauto; simpl; auto); *)
+      (*            apply H1 in HPle; inversion HPle; *)
+      (*            rewrite H2 in *; discriminate *)
+      (*          ). *)
+
+      (* + econstructor. split. *)
+      (* apply Smallstep.plus_one. *)
+      (* eapply HTL.step_module; eauto. *)
+      (* econstructor; simpl; trivial. *)
+      (* constructor; trivial. *)
+      (* econstructor; simpl; eauto. *)
+      (* eapply eval_correct; eauto. constructor. *)
+      (* unfold_merge. simpl. *)
+      (* rewrite AssocMap.gso. *)
+      (* apply AssocMap.gss. *)
+      (* apply st_greater_than_res. *)
+
+      (* (* match_states *) *)
+      (* assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit. *)
+      (* rewrite <- H1. *)
+      (* constructor; auto. *)
+      (* unfold_merge. *)
+      (* apply regs_lessdef_add_match. *)
+      (* constructor. *)
+      (* apply regs_lessdef_add_greater. *)
+      (* apply greater_than_max_func. *)
+      (* assumption. *)
+
+      (* unfold state_st_wf. intros. inversion H2. subst. *)
+      (* unfold_merge. *)
+      (* rewrite AssocMap.gso. *)
+      (* apply AssocMap.gss. *)
+      (* apply st_greater_than_res. *)
+
+      (* + econstructor. split. *)
+      (* apply Smallstep.plus_one. *)
+      (* eapply HTL.step_module; eauto. *)
+      (* econstructor; simpl; trivial. *)
+      (* constructor; trivial. *)
+      (* econstructor; simpl; eauto. *)
+      (* eapply eval_correct; eauto. *)
+      (* constructor. rewrite valueToInt_intToValue. trivial. *)
+      (* unfold_merge. simpl. *)
+      (* rewrite AssocMap.gso. *)
+      (* apply AssocMap.gss. *)
+      (* apply st_greater_than_res. *)
+
+      (* (* match_states *) *)
+      (* assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit. *)
+      (* rewrite <- H1. *)
+      (* constructor. *)
+      (* unfold_merge. *)
+      (* apply regs_lessdef_add_match. *)
+      (* constructor. *)
+      (* symmetry. apply valueToInt_intToValue. *)
+      (* apply regs_lessdef_add_greater. *)
+      (* apply greater_than_max_func. *)
+      (* assumption. assumption. *)
+
+      (* unfold state_st_wf. intros. inversion H2. subst. *)
+      (* unfold_merge. *)
+      (* rewrite AssocMap.gso. *)
+      (* apply AssocMap.gss. *)
+      (* apply st_greater_than_res. *)
+      (* assumption. *)
+      admit.
+
+    - admit.
+    - admit.
+
+    - eexists. split. apply Smallstep.plus_one.
       eapply HTL.step_module; eauto.
-      econstructor; simpl; trivial.
-      constructor; trivial.
-      econstructor; simpl; eauto.
-      eapply eval_correct; eauto.
-      constructor. rewrite valueToInt_intToValue. trivial.
-      unfold_merge. simpl.
-      rewrite AssocMap.gso.
-      apply AssocMap.gss.
-      apply st_greater_than_res.
+      eapply Verilog.stmnt_runp_Vnonblock_reg with
+          (rhsval := if b then posToValue 32 ifso else posToValue 32 ifnot).
 
-      (* match_states *)
-      assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit.
-      rewrite <- H1.
       constructor.
-      unfold_merge.
-      apply regs_lessdef_add_match.
-      constructor.
-      symmetry. apply valueToInt_intToValue.
-      apply regs_lessdef_add_greater.
-      apply greater_than_max_func.
-      assumption. assumption.
 
-      unfold state_st_wf. intros. inversion H2. subst.
-      unfold_merge.
-      rewrite AssocMap.gso.
-      apply AssocMap.gss.
-      apply st_greater_than_res.
-      assumption.
-
-      - econstructor. split. apply Smallstep.plus_one.
-      eapply HTL.step_module; eauto.
-      eapply Verilog.stmnt_runp_Vnonblock with
-          (rhsval := if b then posToValue 32 ifso else posToValue 32 ifnot).
-      simpl. trivial.
+      simpl.
       destruct b.
       eapply Verilog.erun_Vternary_true.
       eapply eval_cond_correct; eauto.
@@ -388,12 +410,9 @@ Section CORRECTNESS.
       eapply eval_cond_correct; eauto.
       constructor.
       apply boolToValue_ValueToBool.
-      trivial.
       constructor.
-      trivial.
       unfold_merge.
       apply AssocMap.gss.
-      trivial.
 
       destruct b.
       rewrite assumption_32bit.
@@ -406,6 +425,9 @@ Section CORRECTNESS.
       subst. unfold_merge.
       apply AssocMap.gss.
       assumption.
+
+      assumption.
+
       rewrite assumption_32bit.
       apply match_state.
       unfold_merge.
@@ -417,6 +439,8 @@ Section CORRECTNESS.
       apply AssocMap.gss.
       assumption.
 
+      assumption.
+
     - (* Return *)
       econstructor. split.
       eapply Smallstep.plus_two.
@@ -428,12 +452,15 @@ Section CORRECTNESS.
       constructor.
       econstructor; simpl; trivial.
       constructor.
-      unfold_merge.
-      trivial.
+
+      constructor.
+      constructor.
+
+      unfold_merge. simpl.
       rewrite AssocMap.gso.
       rewrite AssocMap.gso.
-      unfold state_st_wf in WF. eapply WF. trivial.
-      apply st_greater_than_res. apply st_greater_than_res. trivial.
+      unfold state_st_wf in WF. eapply WF. reflexivity.
+      apply st_greater_than_res. apply st_greater_than_res.
 
       apply HTL.step_finish.
       unfold_merge; simpl.
@@ -441,21 +468,24 @@ Section CORRECTNESS.
       apply AssocMap.gss.
       apply finish_not_return.
       apply AssocMap.gss.
-      rewrite Events.E0_left. trivial.
+      rewrite Events.E0_left. reflexivity.
       constructor.
       assumption.
       constructor.
-    - inversion H11. subst.
-      econstructor. split.
+
+    - econstructor. split.
       eapply Smallstep.plus_two.
       eapply HTL.step_module; eauto.
       constructor.
       econstructor; simpl; trivial.
       econstructor; simpl; trivial.
+
+      constructor. constructor.
+
       constructor.
       econstructor; simpl; trivial.
       apply Verilog.erun_Vvar. trivial.
-      unfold_merge.
+      unfold_merge. simpl.
       rewrite AssocMap.gso.
       rewrite AssocMap.gso.
       unfold state_st_wf in WF. eapply WF. trivial.
@@ -482,6 +512,9 @@ Section CORRECTNESS.
       apply greater_than_max_func.
       apply init_reg_assoc_empty. assumption. unfold state_st_wf.
       intros. inv H1. apply AssocMap.gss. constructor.
+
+      admit.
+
     - inversion MSTATE; subst. inversion MS; subst. econstructor.
       split. apply Smallstep.plus_one.
       constructor.
@@ -492,15 +525,19 @@ 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).
-      exact (ZToValue 32 0).
-      exact (AssocMap.empty value).
-      exact (AssocMap.empty value).
-      exact (AssocMap.empty value).
-      exact (AssocMap.empty value).
-  Qed.
+      admit.
+      admit.
+      (* exact (ZToValue 32 0). *)
+      (* exact (AssocMap.empty value). *)
+      (* exact (AssocMap.empty value). *)
+      (* exact (AssocMap.empty value). *)
+      (* exact (AssocMap.empty value). *)
+  Admitted.
   Hint Resolve transl_step_correct : htlproof.
 
   Lemma transl_initial_states :
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index afc6f72..4bf3843 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -136,68 +136,93 @@ Inductive tr_op : Op.operation -> list reg -> expr -> Prop :=
 | tr_op_Oshr : forall r1 r2, tr_op Op.Oshr (r1::r2::nil) (bop Vshr r1 r2)
 | tr_op_Oshrimm : forall n r, tr_op (Op.Oshrimm n) (r::nil) (boplit Vshr r n)
 | tr_op_Ocmp : forall c l e s s' i, translate_condition c l s = OK e s' i -> tr_op (Op.Ocmp c) l e
-| tr_op_Olea : forall a l e s s' i, translate_eff_addressing a l s = OK e s' i -> tr_op (Op.Olea a) l e.
+| tr_op_Olea : forall a l e s s' i, translate_eff_addressing a l s = OK e s' i -> tr_op (Op.Olea a) l e
+| tr_op_Oleal : forall a l e s s' i, translate_eff_addressing a l s = OK e s' i -> tr_op (Op.Oleal a) l e
+| tr_op_Ocast32signed : forall r, tr_op (Op.Ocast32signed) (r::nil) (Vvar r).
 Hint Constructors tr_op : htlspec.
 
-Inductive tr_instr (fin rtrn st : reg) : RTL.instruction -> stmnt -> stmnt -> Prop :=
+Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt -> Prop :=
 | tr_instr_Inop :
     forall n,
-      tr_instr fin rtrn st (RTL.Inop n) Vskip (state_goto st n)
+      tr_instr fin rtrn st stk (RTL.Inop n) Vskip (state_goto st n)
 | tr_instr_Iop :
     forall n op args e dst,
       tr_op op args e ->
-      tr_instr fin rtrn st (RTL.Iop op args dst n) (Vnonblock (Vvar dst) e) (state_goto st n)
+      tr_instr fin rtrn st stk (RTL.Iop op args dst n) (Vnonblock (Vvar dst) e) (state_goto st n)
 | tr_instr_Icond :
     forall n1 n2 cond args s s' i c,
       translate_condition cond args s = OK c s' i ->
-      tr_instr fin rtrn st (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2)
+      tr_instr fin rtrn st stk (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2)
 | tr_instr_Ireturn_None :
-    tr_instr fin rtrn st (RTL.Ireturn None) (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z)))
+    tr_instr fin rtrn st stk (RTL.Ireturn None) (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z)))
                                                   (block rtrn (Vlit (ZToValue 1%nat 0%Z)))) Vskip
 | tr_instr_Ireturn_Some :
     forall r,
-      tr_instr fin rtrn st (RTL.Ireturn (Some r))
-               (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r))) Vskip.
+      tr_instr fin rtrn st stk (RTL.Ireturn (Some r))
+               (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r))) Vskip
+| 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_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))
+               (state_goto st n).
 Hint Constructors tr_instr : htlspec.
 
 Inductive tr_code (c : RTL.code) (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PTree.t stmnt)
-          (fin rtrn st : reg) : Prop :=
+          (fin rtrn st stk : reg) : Prop :=
   tr_code_intro :
     forall s t,
       c!pc = Some i ->
       stmnts!pc = Some s ->
       trans!pc = Some t ->
-      tr_instr fin rtrn st i s t ->
-      tr_code c pc i stmnts trans fin rtrn st.
+      tr_instr fin rtrn st stk i s t ->
+      tr_code c pc i stmnts trans fin rtrn st stk.
 Hint Constructors tr_code : htlspec.
 
 Inductive tr_module (f : RTL.function) : module -> Prop :=
   tr_module_intro :
-    forall data control fin rtrn st m,
+    forall data control fin rtrn st stk m,
       (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) ->
+                    tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) ->
       m = (mkmodule f.(RTL.fn_params)
                         data
                         control
                         f.(RTL.fn_entrypoint)
-                            st fin rtrn) ->
+                            st stk fin rtrn) ->
       tr_module f m.
 Hint Constructors tr_module : htlspec.
 
 Lemma create_reg_datapath_trans :
-  forall s s' x i,
-    create_reg s = OK x s' i ->
+  forall sz s s' x i,
+    create_reg sz s = OK x s' i ->
     s.(st_datapath) = s'.(st_datapath).
 Proof. intros. monadInv H. trivial. Qed.
 Hint Resolve create_reg_datapath_trans : htlspec.
 
 Lemma create_reg_controllogic_trans :
-  forall s s' x i,
-    create_reg s = OK x s' i ->
+  forall sz s s' x i,
+    create_reg sz s = OK x s' i ->
     s.(st_controllogic) = s'.(st_controllogic).
 Proof. intros. monadInv H. trivial. Qed.
 Hint Resolve create_reg_controllogic_trans : htlspec.
 
+Lemma create_arr_datapath_trans :
+  forall sz ln s s' x i,
+    create_arr sz ln s = OK x s' i ->
+    s.(st_datapath) = s'.(st_datapath).
+Proof. intros. monadInv H. trivial. Qed.
+Hint Resolve create_arr_datapath_trans : htlspec.
+
+Lemma create_arr_controllogic_trans :
+  forall sz ln s s' x i,
+    create_arr sz ln s = OK x s' i ->
+    s.(st_controllogic) = s'.(st_controllogic).
+Proof. intros. monadInv H. trivial. Qed.
+Hint Resolve create_arr_controllogic_trans : htlspec.
+
 Lemma get_refl_x :
   forall s s' x i,
     get s = OK x s' i ->
@@ -214,10 +239,14 @@ Hint Resolve get_refl_s : htlspec.
 
 Ltac inv_incr :=
   repeat match goal with
-  | [ H: create_reg ?s = OK _ ?s' _ |- _ ] =>
+  | [ H: create_reg _ ?s = OK _ ?s' _ |- _ ] =>
     let H1 := fresh "H" in
     assert (H1 := H); eapply create_reg_datapath_trans in H;
     eapply create_reg_controllogic_trans in H1
+  | [ H: create_arr _ _ ?s = OK _ ?s' _ |- _ ] =>
+    let H1 := fresh "H" in
+    assert (H1 := H); eapply create_arr_datapath_trans in H;
+    eapply create_arr_controllogic_trans in H1
   | [ H: get ?s = OK _ _ _ |- _ ] =>
     let H1 := fresh "H" in
     assert (H1 := H); apply get_refl_x in H; apply get_refl_s in H1;
@@ -281,56 +310,69 @@ Ltac destruct_optional :=
   match goal with H: option ?r |- _ => destruct H end.
 
 Lemma iter_expand_instr_spec :
-  forall l fin rtrn s s' i x c,
-    HTLMonadExtra.collectlist (transf_instr fin rtrn) l s = OK x s' i ->
+  forall l fin rtrn stack s s' i x c,
+    HTLMonadExtra.collectlist (transf_instr fin rtrn stack) l s = OK x s' i ->
     list_norepet (List.map fst l) ->
     (forall pc instr, In (pc, instr) l -> c!pc = Some instr) ->
     (forall pc instr, In (pc, instr) l ->
                       c!pc = Some instr ->
-                      tr_code c pc instr s'.(st_datapath) s'.(st_controllogic) fin rtrn s'.(st_st)).
+                      tr_code c pc instr s'.(st_datapath) s'.(st_controllogic) fin rtrn s'.(st_st) stack).
 Proof.
   induction l; simpl; intros; try contradiction.
   destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr.
   destruct (peq pc pc1).
-  + subst.
+  - subst.
     destruct instr1 eqn:?; try discriminate;
       try destruct_optional; inv_add_instr; econstructor; try assumption.
-    * destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9;
-        [ discriminate | apply H9 ].
-    * destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9;
-        [ discriminate | apply H9 ].
-    * inversion H2. inversion H9. rewrite H. apply tr_instr_Inop.
-      eapply in_map with (f := fst) in H9; contradiction.
-
-    * destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9;
-        [ discriminate | apply H9 ].
-    * destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9;
-        [ discriminate | apply H9 ].
-    * inversion H2. inversion H9. unfold nonblock. rewrite <- e2. rewrite H. constructor.
-      eapply translate_instr_tr_op. apply EQ1. eapply in_map with (f := fst) in H9. contradiction.
-
-    * destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9;
-        [ discriminate | apply H9 ].
-    * destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9;
-        [ discriminate | apply H9 ].
-    * inversion H2. inversion H9. rewrite <- e2. rewrite H. econstructor. apply EQ1.
+    + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
+    + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
+    + inversion H2. inversion H9. rewrite H. apply tr_instr_Inop.
       eapply in_map with (f := fst) in H9. contradiction.
 
-    * destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9;
-        [ discriminate | apply H9 ].
-    * destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9;
-        [ discriminate | apply H9 ].
-    * inversion H2. inversion H9. constructor.
+    + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
+    + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
+    + inversion H2. inversion H9. unfold nonblock. rewrite <- e2. rewrite H. constructor.
+      eapply translate_instr_tr_op. apply EQ1.
       eapply in_map with (f := fst) in H9. contradiction.
 
-    * destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9;
-        [ discriminate | apply H9 ].
-    * destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9;
-        [ discriminate | apply H9 ].
-    * inversion H2. inversion H9. constructor.
+    + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
+    + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
+    + inversion H2. inversion H9. rewrite <- e2. rewrite H. econstructor. apply EQ1.
       eapply in_map with (f := fst) in H9. contradiction.
 
-  + eapply IHl. apply EQ0. assumption.
+    + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
+    + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
+    + destruct H2.
+      * inversion H2.
+        replace (st_st s2) with (st_st s0) by congruence.
+        eauto with htlspec.
+      * apply in_map with (f := fst) in H2. contradiction.
+
+    + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
+    + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
+    + destruct H2.
+      * inversion H2.
+        replace (st_st s2) with (st_st s0) by congruence.
+        eauto with htlspec.
+      * apply in_map with (f := fst) in H2. contradiction.
+
+    + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
+    + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
+    + inversion H2.
+      * inversion H9.
+        replace (st_st s2) with (st_st s0) by congruence.
+        eauto with htlspec.
+      * apply in_map with (f := fst) in H9. contradiction.
+
+    + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
+    + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
+    + inversion H2.
+      * inversion H9.
+        replace (st_st s2) with (st_st s0) by congruence.
+        eauto with htlspec.
+      * apply in_map with (f := fst) in H9. contradiction.
+
+  - eapply IHl. apply EQ0. assumption.
     destruct H2. inversion H2. subst. contradiction.
     intros. specialize H1 with pc0 instr0. destruct H1. tauto. trivial.
     destruct H2. inv H2. contradiction. assumption. assumption.
@@ -353,9 +395,9 @@ Proof.
   econstructor; simpl; trivial.
   intros.
   inv_incr.
-  assert (STC: st_controllogic s8 = st_controllogic s2) by congruence.
-  assert (STD: st_datapath s8 = st_datapath s2) by congruence.
-  assert (STST: st_st s8 = st_st s2) by congruence.
+  assert (STC: st_controllogic s9 = st_controllogic s3) by congruence.
+  assert (STD: st_datapath s9 = st_datapath s3) by congruence.
+  assert (STST: st_st s9 = st_st s3) by congruence.
   rewrite STC. rewrite STD. rewrite STST.
   eapply iter_expand_instr_spec; eauto with htlspec.
   apply PTree.elements_complete.
diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v
index f127b11..4a6f23e 100644
--- a/src/translation/Veriloggen.v
+++ b/src/translation/Veriloggen.v
@@ -61,12 +61,17 @@ Definition states_have_transitions (stm: PositiveMap.t stmnt) (st: PositiveMap.t
       /\ (forall x, st!n = Some x -> exists y, stm!n = Some y).
 Hint Unfold states_have_transitions : verilog_state.
 
+Record decl : Type := mkdecl {
+  width: nat;
+  length: nat
+}.
+
 Record state: Type := mkstate {
   st_freshreg: reg;
   st_freshstate: node;
   st_stm: PositiveMap.t stmnt;
   st_statetrans: PositiveMap.t statetrans;
-  st_decl: PositiveMap.t nat;
+  st_decl: PositiveMap.t decl;
   st_wf: valid_freshstate st_stm st_freshstate
          /\ states_have_transitions st_stm st_statetrans;
 }.
@@ -94,7 +99,7 @@ Definition init_state : state :=
           1%positive
           (PositiveMap.empty stmnt)
           (PositiveMap.empty statetrans)
-          (PositiveMap.empty nat)
+          (PositiveMap.empty decl)
           init_state_wf.
 
 Inductive state_incr: state -> state -> Prop :=
@@ -204,7 +209,7 @@ 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 32%nat l)).
+  Vbinop op (Vvar r) (Vlit (ZToValue 32 l)).
 
 Definition translate_comparison (c : Integers.comparison) (args : list reg) : mon expr :=
   match c, args with
@@ -245,9 +250,14 @@ Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon ex
   | Op.Aindexed off, r1::nil => ret (boplitz Vadd r1 off)
   | Op.Aindexed2 off, r1::r2::nil => ret (Vbinop Vadd (Vvar r1) (boplitz Vadd r2 off))
   | Op.Ascaled scale offset, r1::nil =>
-    ret (Vbinop Vadd (boplitz Vadd r1 scale) (Vlit (ZToValue 32%nat offset)))
+    ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue 32 offset)))
   | Op.Aindexed2scaled scale offset, r1::r2::nil =>
     ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale))
+  (* Stack arrays/referenced variables *)
+  | 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 (Vlit (ZToValue 32 (a / 4)))
+    else error (Errors.msg "Veriloggen: eff_addressing misaligned stack offset")
   | _, _ => error (Errors.msg "Veriloggen: eff_addressing instruction not implemented: other")
   end.
 
@@ -284,6 +294,8 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr :=
   | Op.Oshldimm n, r::nil => error (Errors.msg "Veriloggen: Instruction not implemented: Oshldimm")
   | Op.Ocmp c, _ => translate_condition c args
   | Op.Olea a, _ => translate_eff_addressing a args
+  | Op.Oleal a, _ => translate_eff_addressing a args (* FIXME: Need to be careful here; large arrays might fail? *)
+  | Op.Ocast32signed, r::nill => ret (Vvar r) (* FIXME: Don't need to sign extend for now since everything is 32 bit? *)
   | _, _ => error (Errors.msg "Veriloggen: Instruction not implemented: other")
   end.
 
@@ -380,7 +392,7 @@ Definition add_reg (r: reg) (s: state) : state :=
           (st_freshstate s)
           (st_stm s)
           (st_statetrans s)
-          (PositiveMap.add r 32%nat (st_decl s))
+          (PositiveMap.add r (mkdecl 32 0) (st_decl s))
           (st_wf s).
 
 Lemma add_reg_state_incr:
@@ -417,9 +429,9 @@ Proof. constructor; simpl; auto using Ple_succ with verilog_state. Qed.
 (** Declare a new register by incrementing the [st_freshreg] by one and
 returning the old [st_freshreg]. *)
 
-Definition decl_io (sz: nat): mon (reg * nat) :=
+Definition decl_io (d: decl) : mon (reg * decl) :=
   fun s => let r := s.(st_freshreg) in
-           OK (r, sz) (mkstate
+           OK (r, d) (mkstate
                      (Pos.succ r)
                      (st_freshstate s)
                      (st_stm s)
@@ -431,22 +443,22 @@ Definition decl_io (sz: nat): mon (reg * nat) :=
 (** Declare a new register which is given, by changing [st_decl] and without
 affecting anything else. *)
 
-Definition declare_reg (r: reg) (sz: nat): mon (reg * nat) :=
-  fun s => OK (r, sz) (mkstate
+Definition declare_reg (r: reg) (d: decl): mon (reg * decl) :=
+  fun s => OK (r, d) (mkstate
                       (st_freshreg s)
                       (st_freshstate s)
                       (st_stm s)
                       (st_statetrans s)
-                      (PositiveMap.add r sz s.(st_decl))
+                      (PositiveMap.add r d s.(st_decl))
                       (st_wf s))
-              (change_decl_state_incr s (PositiveMap.add r sz s.(st_decl))).
+              (change_decl_state_incr s (PositiveMap.add r d s.(st_decl))).
 
 (** Declare a new fresh register by first getting a valid register to increment,
 and then adding it to the declaration list. *)
 
-Definition decl_fresh_reg (sz : nat) : mon (reg * nat) :=
-  do (r, s) <- decl_io sz;
-  declare_reg r s.
+Definition decl_fresh_reg (d: decl) : mon (reg * decl) :=
+  do (r, d) <- decl_io d;
+  declare_reg r d.
 
 Lemma add_branch_instr_states_have_transitions:
   forall s e n n1 n2,
@@ -512,7 +524,26 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit :=
     | _, _, _ => Error (Errors.msg "Veriloggen: add_branch_instr")
     end.
 
-Definition transf_instr (fin rtrn: reg) (ni: node * instruction) : 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 => ret (Vvari stack (boplitz Vadd r1 off)) (* FIXME: Cannot guarantee alignment *)
+  | 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 "Veriloggen: translate_arr_access address misaligned")
+  | 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 (boplitz Vadd r1 (offset / 4)) (boplitz Vmul r2 (scale / 4))))
+    else error (Errors.msg "Veriloggen: translate_arr_access address misaligned")
+  | 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 "Veriloggen: eff_addressing misaligned stack offset")
+  | _, _ => error (Errors.msg "Veriloggen: translate_arr_access unsuported addressing")
+  end.
+
+Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit :=
   match ni with
     (n, i) =>
     match i with
@@ -520,8 +551,12 @@ Definition transf_instr (fin rtrn: reg) (ni: node * instruction) : mon unit :=
     | Iop op args dst n' =>
       do instr <- translate_instr op args;
       add_instr_reg dst n n' (block dst instr)
-    | Iload _ _ _ _ _ => error (Errors.msg "Loads are not implemented.")
-    | Istore _ _ _ _ _ => error (Errors.msg "Stores are not implemented.")
+    | Iload mem addr args dst n' =>
+      do src <- translate_arr_access mem addr args stack;
+      add_instr_reg dst n n' (block dst src)
+    | Istore mem addr args src n' =>
+      do dst <- translate_arr_access mem addr args stack;
+      add_instr_reg src n n' (Vblock 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.")
@@ -554,8 +589,11 @@ Definition make_statetrans_cases (r : reg) (st : positive * statetrans) : expr *
 Definition make_statetrans (r : reg) (s : PositiveMap.t statetrans) : stmnt :=
   Vcase (Vvar r) (map (make_statetrans_cases r) (PositiveMap.elements s)) (Some Vskip).
 
-Definition allocate_reg (e : reg * nat) : module_item :=
-  match e with (r, n) => Vdecl r n end.
+Definition allocate_reg (e : reg * decl) : module_item :=
+  match e with
+  | (r, (mkdecl n 0)) => Vdecl r n
+  | (r, (mkdecl n l)) => Vdeclarr r n l
+  end.
 
 Definition make_module_items (entry: node) (clk st rst: reg) (s: state) : list module_item :=
   (Valways_ff (Vposedge clk)
@@ -570,17 +608,22 @@ Definition make_module_items (entry: node) (clk st rst: reg) (s: state) : list m
 
 Definition set_int_size (r: reg) : reg * nat := (r, 32%nat).
 
+(*FIXME: This shouldn't be necessary; needs alterations in Verilog.v *)
+Definition get_sz (rg : reg * decl) : szreg := match rg with (r, d) => (r, d.(width)) end.
+
 Definition transf_module (f: function) : mon module :=
-  do fin <- decl_io 1;
-  do rtrn <- decl_io 32;
-  do _ <- traverselist (transf_instr (fst fin) (fst rtrn)) (Maps.PTree.elements f.(fn_code));
-  do start <- decl_io 1;
-  do rst <- decl_io 1;
-  do clk <- decl_io 1;
-  do st <- decl_fresh_reg 32;
+  do fin <- decl_io (mkdecl 1 0);
+  do rtrn <- decl_io (mkdecl 32 0);
+  do stack <- decl_fresh_reg (mkdecl 32%nat (Z.to_nat (f.(fn_stacksize) / 4)));
+  do _ <- traverselist (transf_instr (fst fin) (fst rtrn) (fst stack)) (Maps.PTree.elements f.(fn_code));
+  do start <- decl_io (mkdecl 1 0);
+  do rst <- decl_io (mkdecl 1 0);
+  do clk <- decl_io (mkdecl 1 0);
+  do st <- decl_fresh_reg (mkdecl 32 0);
   do current_state <- get;
   let mi := make_module_items f.(fn_entrypoint) (fst clk) (fst st) (fst rst) current_state in
-  ret (mkmodule start rst clk fin rtrn st (map set_int_size f.(fn_params)) mi).
+  ret (mkmodule (get_sz start) (get_sz rst) (get_sz clk) (get_sz fin) (get_sz rtrn) (get_sz st)
+                (map set_int_size f.(fn_params)) mi).
 
 Lemma max_state_valid_freshstate:
   forall f,
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
index 82378b3..2e4ef1a 100644
--- a/src/verilog/HTL.v
+++ b/src/verilog/HTL.v
@@ -45,6 +45,7 @@ Record module: Type :=
     mod_controllogic : controllogic;
     mod_entrypoint : node;
     mod_st : reg;
+    mod_stk : reg;
     mod_finish : reg;
     mod_return : reg
   }.
@@ -76,7 +77,8 @@ Inductive state : Type :=
     forall (stack : list stackframe)
            (m : module)
            (st : node)
-           (assoc : assocmap), state
+           (reg_assoc : assocmap)
+           (arr_assoc : AssocMap.t (list value)), state
 | Returnstate :
     forall (res : list stackframe)
            (v : value), state
@@ -87,38 +89,49 @@ Inductive state : Type :=
 
 Inductive step : genv -> state -> Events.trace -> state -> Prop :=
 | step_module :
-    forall g m st ctrl data assoc0 assoc1 assoc2
-           assoc3 nbassoc0 nbassoc1 f stval pstval sf,
+    forall g m st sf ctrl data
+      asr asa
+      basr1 basa1 nasr1 nasa1
+      basr2 basa2 nasr2 nasa2
+      asr' asa'
+      f stval pstval,
       m.(mod_controllogic)!st = Some ctrl ->
       m.(mod_datapath)!st = Some data ->
       Verilog.stmnt_runp f
-        (Verilog.mkassociations assoc0 empty_assocmap)
+        (Verilog.mkassociations asr empty_assocmap)
+        (Verilog.mkassociations asa (AssocMap.empty (list value)))
         ctrl
-        (Verilog.mkassociations assoc1 nbassoc0) ->
+        (Verilog.mkassociations basr1 nasr1)
+        (Verilog.mkassociations basa1 nasa1) ->
       Verilog.stmnt_runp f
-        (Verilog.mkassociations assoc1 nbassoc0)
+        (Verilog.mkassociations basr1 nasr1)
+        (Verilog.mkassociations basa1 nasa1)
         data
-        (Verilog.mkassociations assoc2 nbassoc1) ->
-      assoc3 = merge_assocmap nbassoc1 assoc2 ->
-      assoc3!(m.(mod_st)) = Some stval ->
+        (Verilog.mkassociations basr2 nasr2)
+        (Verilog.mkassociations basa2 nasa2) ->
+      asr' = merge_assocmap nasr2 basr2 ->
+      asa' = AssocMapExt.merge (list value) nasa2 basa2 ->
+      asr'!(m.(mod_st)) = Some stval ->
       valueToPos stval = pstval ->
-      step g (State sf m st assoc0) Events.E0 (State sf m pstval assoc3)
+      step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa')
 | step_finish :
-    forall g m st assoc retval sf,
-    assoc!(m.(mod_finish)) = Some (1'h"1") ->
-    assoc!(m.(mod_return)) = Some retval ->
-    step g (State sf m st assoc) Events.E0 (Returnstate sf retval)
+    forall g m st asr asa retval sf,
+    asr!(m.(mod_finish)) = Some (1'h"1") ->
+    asr!(m.(mod_return)) = Some retval ->
+    step g (State sf m st asr asa) Events.E0 (Returnstate sf retval)
 | step_call :
     forall g m args res,
       step g (Callstate res m args) Events.E0
            (State res m m.(mod_entrypoint)
              (AssocMap.set (mod_st m) (posToValue 32 m.(mod_entrypoint))
-               (init_regs args m.(mod_params))))
+                           (init_regs args m.(mod_params)))
+              (AssocMap.empty (list value)))
 | step_return :
-    forall g m assoc i r sf pc mst,
+    forall g m asr i r sf pc mst,
       mst = mod_st m ->
-      step g (Returnstate (Stackframe r m pc assoc :: sf) i) Events.E0
-           (State sf m pc ((assoc # mst <- (posToValue 32 pc)) # r <- i)).
+      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))).
 Hint Constructors step : htl.
 
 Inductive initial_state (p: program): state -> Prop :=
diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml
index 29c4f5a..bdd8581 100644
--- a/src/verilog/PrintVerilog.ml
+++ b/src/verilog/PrintVerilog.ml
@@ -70,6 +70,7 @@ let literal l = sprintf "%d'd%d" (Nat.to_int l.vsize) (Z.to_int (uvalueToZ l))
 let rec pprint_expr = function
   | Vlit l -> literal l
   | Vvar s -> register s
+  | Vvari (s, i) -> concat [register s; "["; pprint_expr i; "]"]
   | Vinputvar s -> register s
   | Vunop (u, e) -> concat ["("; unop u; pprint_expr e; ")"]
   | Vbinop (op, a, b) -> concat ["("; pprint_binop (pprint_expr a) (pprint_expr b) op; ")"]
@@ -111,9 +112,16 @@ let declare i t =
     concat [ indent i; t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] ";
              register r; ";\n" ]
 
+let declarearr i t =
+  function (r, sz, ln) ->
+    concat [ indent i; t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] ";
+             register r;
+             " ["; sprintf "%d" (Nat.to_int ln - 1); ":0];\n" ]
+
 (* TODO Fix always blocks, as they currently always print the same. *)
 let pprint_module_item i = function
   | Vdecl (r, sz) -> declare i "reg" (r, sz)
+  | Vdeclarr (r, sz, ln) -> declarearr i "reg" (r, sz, ln)
   | Valways (e, s) ->
     concat [indent i; "always "; pprint_edge_top i e; "\n"; pprint_stmnt (i+1) s]
   | Valways_ff (e, s) ->
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index cccdf9a..845d706 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -35,16 +35,59 @@ Import HexNotationValue.
 
 Local Open Scope assocmap.
 
+Set Implicit Arguments.
+
 Definition reg : Type := positive.
 Definition node : Type := positive.
 Definition szreg : Type := reg * nat.
 
-Record associations : Type :=
+Record associations (A : Type) : Type :=
   mkassociations {
-    assoc_blocking : assocmap;
-    assoc_nonblocking : assocmap
+    assoc_blocking : AssocMap.t A;
+    assoc_nonblocking : AssocMap.t A
   }.
 
+Definition reg_associations := associations value.
+Definition arr_associations := associations (list value).
+
+Definition assocmap_arr := AssocMap.t (list value).
+
+Definition merge_associations {A : Type} (assoc : associations A) :=
+  mkassociations (AssocMapExt.merge A assoc.(assoc_nonblocking) assoc.(assoc_blocking))
+                 (AssocMap.empty A).
+
+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
+  end.
+
+Definition assocmap_l_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
+  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).
+
+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)).
+
+Definition block_reg (r : reg) (asr : reg_associations) (v : value) :=
+  mkassociations (AssocMap.set r v asr.(assoc_blocking)) asr.(assoc_nonblocking).
+
+Definition nonblock_reg (r : reg) (asr : reg_associations) (v : value) :=
+  mkassociations asr.(assoc_blocking) (AssocMap.set r v asr.(assoc_nonblocking)).
+
+
 (** * Verilog AST
 
 The Verilog AST is defined here, which is the target language of the
@@ -98,6 +141,7 @@ Inductive unop : Type :=
 Inductive expr : Type :=
 | Vlit : value -> expr
 | Vvar : reg -> expr
+| Vvari : reg -> expr -> expr
 | Vinputvar : reg -> expr
 | Vbinop : binop -> expr -> expr -> expr
 | Vunop : unop -> expr -> expr
@@ -139,6 +183,7 @@ done using combinational always block instead of continuous assignments. *)
 
 Inductive module_item : Type :=
 | Vdecl : reg -> nat -> module_item
+| Vdeclarr : reg -> nat -> nat -> module_item
 | Valways : edge -> stmnt -> module_item
 | Valways_ff : edge -> stmnt -> module_item
 | Valways_comb : edge -> stmnt -> module_item.
@@ -199,8 +244,8 @@ retrieved and set appropriately.
 Inductive state : Type :=
 | State:
     forall (m : module)
-           (assoc : assocmap)
-           (nbassoc : assocmap)
+           (assoc : reg_associations)
+           (assoc : arr_associations)
            (f : fextclk)
            (cycle : nat)
            (stvar : value),
@@ -241,43 +286,48 @@ Definition unop_run (op : unop) : value -> value :=
   | Vnot => vbitneg
   end.
 
-Inductive expr_runp : fext -> assocmap -> expr -> value -> Prop :=
+Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop :=
   | erun_Vlit :
-      forall fext assoc v,
-      expr_runp fext assoc (Vlit v) v
+      forall fext reg stack v,
+      expr_runp fext reg stack (Vlit v) v
   | erun_Vvar :
-      forall fext assoc v r,
-      assoc#r = v ->
-      expr_runp fext assoc (Vvar r) v
+      forall fext reg stack v r,
+      reg#r = v ->
+      expr_runp fext reg stack (Vvar r) v
+  | erun_Vvari :
+      forall fext reg stack v iexp i r,
+      expr_runp fext reg stack iexp i ->
+      arr_assocmap_lookup stack r (valueToNat i) = Some v ->
+      expr_runp fext reg stack (Vvari r iexp) v
   | erun_Vinputvar :
-      forall fext assoc r v,
+      forall fext reg stack r v,
       fext!r = Some v ->
-      expr_runp fext assoc (Vinputvar r) v
+      expr_runp fext reg stack (Vinputvar r) v
   | erun_Vbinop :
-      forall fext assoc op l r lv rv oper EQ resv,
-      expr_runp fext assoc l lv ->
-      expr_runp fext assoc r rv ->
+      forall fext reg stack op l r lv rv oper EQ resv,
+      expr_runp fext reg stack l lv ->
+      expr_runp fext reg stack r rv ->
       oper = binop_run op ->
       resv = oper lv rv EQ ->
-      expr_runp fext assoc (Vbinop op l r) resv
+      expr_runp fext reg stack (Vbinop op l r) resv
   | erun_Vunop :
-      forall fext assoc u vu op oper resv,
-      expr_runp fext assoc u vu ->
+      forall fext reg stack u vu op oper resv,
+      expr_runp fext reg stack u vu ->
       oper = unop_run op ->
       resv = oper vu ->
-      expr_runp fext assoc (Vunop op u) resv
+      expr_runp fext reg stack (Vunop op u) resv
   | erun_Vternary_true :
-      forall fext assoc c ts fs vc vt,
-      expr_runp fext assoc c vc ->
-      expr_runp fext assoc ts vt ->
+      forall fext reg stack c ts fs vc vt,
+      expr_runp fext reg stack c vc ->
+      expr_runp fext reg stack ts vt ->
       valueToBool vc = true ->
-      expr_runp fext assoc (Vternary c ts fs) vt
+      expr_runp fext reg stack (Vternary c ts fs) vt
   | erun_Vternary_false :
-      forall fext assoc c ts fs vc vf,
-      expr_runp fext assoc c vc ->
-      expr_runp fext assoc fs vf ->
+      forall fext reg stack c ts fs vc vf,
+      expr_runp fext reg stack c vc ->
+      expr_runp fext reg stack fs vf ->
       valueToBool vc = false ->
-      expr_runp fext assoc (Vternary c ts fs) vf.
+      expr_runp fext reg stack (Vternary c ts fs) vf.
 Hint Constructors expr_runp : verilog.
 
 Definition handle_opt {A : Type} (err : errmsg) (val : option A)
@@ -311,6 +361,7 @@ Definition access_fext (f : fext) (r : reg) : res value :=
               | State _ assoc _ _ _ => handle_def (ZToValue 32 0) assoc!r
               | _ => Error (msg "Verilog: Wrong state")
               end
+  | Vvari _ _ => Error (msg "Verilog: variable indexing not modelled")
   | Vinputvar r => access_fext s r
   | Vbinop op l r =>
     let lv := expr_run s l in
@@ -329,14 +380,23 @@ Definition access_fext (f : fext) (r : reg) : res value :=
     if valueToBool cv then expr_run s te else expr_run s fe
   end.*)
 
-(** Return the name of the lhs of an assignment. For now, this function is quite
-simple because only assignment to normal variables is supported and needed. *)
+(** Return the location of the lhs of an assignment. *)
 
-Definition assign_name (e : expr) : res reg :=
-  match e with
-  | Vvar r => OK r
-  | _ => Error (msg "Verilog: expression not supported on lhs of assignment")
-  end.
+Inductive location : Type :=
+| Reg (_ : reg)
+| Array (_ : reg) (_ : nat).
+
+Inductive location_is : fext -> assocmap -> assocmap_arr -> expr -> location -> Prop :=
+| Base : forall f asr asa r, location_is f asr asa (Vvar r) (Reg r)
+| Indexed : forall f asr asa r iexp iv,
+  expr_runp f asr asa iexp iv ->
+  location_is f asr asa (Vvari r iexp) (Array r (valueToNat iv)).
+
+(* Definition assign_name (f : fext) (asr: assocmap) (asa : assocmap_l)  (e : expr) : res reg := *)
+(*   match e with *)
+(*   | Vvar r => OK r *)
+(*   | _ => Error (msg "Verilog: expression not supported on lhs of assignment") *)
+(*   end. *)
 
 (*Fixpoint stmnt_height (st : stmnt) {struct st} : nat :=
   match st with
@@ -406,61 +466,74 @@ Fixpoint stmnt_run' (n : nat) (s : state) (st : stmnt) {struct n} : res state :=
 Definition stmnt_run (s : state) (st : stmnt) : res state :=
   stmnt_run' (stmnt_height st) s st. *)
 
-Inductive stmnt_runp: fext -> associations -> stmnt -> associations -> Prop :=
+Inductive stmnt_runp: fext -> reg_associations -> arr_associations ->
+                      stmnt -> reg_associations -> arr_associations -> Prop :=
 | stmnt_runp_Vskip:
-    forall f a, stmnt_runp f a Vskip a
+    forall f ar al, stmnt_runp f ar al Vskip ar al
 | stmnt_runp_Vseq:
-    forall f st1 st2 as0 as1 as2,
-    stmnt_runp f as0 st1 as1 ->
-    stmnt_runp f as1 st2 as2 ->
-    stmnt_runp f as0 (Vseq st1 st2) as2
+    forall f st1 st2 asr0 asa0 asr1 asa1 asr2 asa2,
+    stmnt_runp f asr0 asa0 st1 asr1 asa1 ->
+    stmnt_runp f asr1 asa1 st2 asr2 asa2 ->
+    stmnt_runp f asr0 asa1 (Vseq st1 st2) asr2 asa2
 | stmnt_runp_Vcond_true:
-    forall as0 as1 f c vc stt stf,
-    expr_runp f as0.(assoc_blocking) c vc ->
+    forall asr0 asa0 asr1 asa1 f c vc stt stf,
+    expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) c vc ->
     valueToBool vc = true ->
-    stmnt_runp f as0 stt as1 ->
-    stmnt_runp f as0 (Vcond c stt stf) as1
+    stmnt_runp f asr0 asa0 stt asr1 asa1 ->
+    stmnt_runp f asr0 asa0 (Vcond c stt stf) asr1 asa1
 | stmnt_runp_Vcond_false:
-    forall as0 as1 f c vc stt stf,
-    expr_runp f as0.(assoc_blocking) c vc ->
+    forall asr0 asa0 asr1 asa1 f c vc stt stf,
+    expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) c vc ->
     valueToBool vc = false ->
-    stmnt_runp f as0 stf as1 ->
-    stmnt_runp f as0 (Vcond c stt stf) as1
+    stmnt_runp f asr0 asa0 stt asr1 asa1 ->
+    stmnt_runp f asr0 asa0 (Vcond c stt stf) asr1 asa1
 | stmnt_runp_Vcase_nomatch:
-    forall e ve as0 f as1 me mve sc cs def,
-    expr_runp f as0.(assoc_blocking) e ve ->
-    expr_runp f as0.(assoc_blocking) me mve ->
+    forall e ve asr0 asa0 f asr1 asa1 me mve sc cs def,
+    expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) e ve ->
+    expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) me mve ->
     mve <> ve ->
-    stmnt_runp f as0 (Vcase e cs def) as1 ->
-    stmnt_runp f as0 (Vcase e ((me, sc)::cs) def) as1
+    stmnt_runp f asr0 asa0 (Vcase e cs def) asr1 asa1 ->
+    stmnt_runp f asr0 asa0 (Vcase e ((me, sc)::cs) def) asr1 asa1
 | stmnt_runp_Vcase_match:
-    forall e ve as0 f as1 me mve sc cs def,
-    expr_runp f as0.(assoc_blocking) e ve ->
-    expr_runp f as0.(assoc_blocking) me mve ->
+    forall e ve asr0 asa0 f asr1 asa1 me mve sc cs def,
+    expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) e ve ->
+    expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) me mve ->
     mve = ve ->
-    stmnt_runp f as0 sc as1 ->
-    stmnt_runp f as0 (Vcase e ((me, sc)::cs) def) as1
+    stmnt_runp f asr0 asa0 sc asr1 asa1 ->
+    stmnt_runp f asr0 asa0 (Vcase e ((me, sc)::cs) def) asr1 asa1
 | stmnt_runp_Vcase_default:
-    forall as0 as1 f st e ve,
-    expr_runp f as0.(assoc_blocking) e ve ->
-    stmnt_runp f as0 st as1 ->
-    stmnt_runp f as0 (Vcase e nil (Some st)) as1
-| stmnt_runp_Vblock:
-    forall lhs name rhs rhsval assoc assoc' nbassoc f,
-    assign_name lhs = OK name ->
-    expr_runp f assoc rhs rhsval ->
-    assoc' = (AssocMap.set name rhsval assoc) ->
-    stmnt_runp f (mkassociations assoc nbassoc)
+    forall asr0 asa0 asr1 asa1 f st e ve,
+    expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) e ve ->
+    stmnt_runp f asr0 asa0 st asr1 asa1 ->
+    stmnt_runp f asr0 asa0 (Vcase e nil (Some st)) asr1 asa1
+| stmnt_runp_Vblock_reg:
+    forall lhs r rhs rhsval asr asa f,
+    location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (Reg r) ->
+    expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval ->
+    stmnt_runp f asr asa
+                 (Vblock lhs rhs)
+                 (block_reg r asr rhsval) asa
+| stmnt_runp_Vnonblock_reg:
+    forall lhs r rhs rhsval asr asa f,
+    location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (Reg r) ->
+    expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval ->
+    stmnt_runp f asr asa
+                 (Vnonblock lhs rhs)
+                 (nonblock_reg r asr rhsval) asa
+| stmnt_runp_Vblock_arr:
+    forall lhs r i rhs rhsval asr asa f,
+    location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (Array r i) ->
+    expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval ->
+    stmnt_runp f asr asa
                  (Vblock lhs rhs)
-                 (mkassociations assoc' nbassoc)
-| stmnt_runp_Vnonblock:
-    forall lhs name rhs rhsval assoc nbassoc nbassoc' f,
-    assign_name lhs = OK name ->
-    expr_runp f assoc rhs rhsval ->
-    nbassoc' = (AssocMap.set name rhsval nbassoc) ->
-    stmnt_runp f (mkassociations assoc nbassoc)
+                 asr (block_arr r i asa rhsval)
+| stmnt_runp_Vnonblock_arr:
+    forall lhs r i rhs rhsval asr asa f,
+    location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (Array r i) ->
+    expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval ->
+    stmnt_runp f asr asa
                  (Vnonblock lhs rhs)
-                 (mkassociations assoc nbassoc').
+                 asr (nonblock_arr r i asa rhsval).
 Hint Constructors stmnt_runp : verilog.
 
 (*Fixpoint mi_step (s : state) (m : list module_item) {struct m} : res state :=
@@ -473,36 +546,39 @@ Hint Constructors stmnt_runp : verilog.
   | (Valways_ff _ st)::ls => run st ls
   | (Valways_comb _ st)::ls => run st ls
   | (Vdecl _ _)::ls => mi_step s ls
+  | (Vdeclarr _ _ _)::ls => mi_step s ls
   | nil => OK s
   end.*)
 
-Inductive mi_stepp : fext -> associations -> module_item -> associations -> Prop :=
+Inductive mi_stepp : fext -> reg_associations -> arr_associations ->
+                     module_item -> reg_associations -> arr_associations -> Prop :=
 | mi_stepp_Valways :
-    forall f s0 st s1 c,
-    stmnt_runp f s0 st s1 ->
-    mi_stepp f s0 (Valways c st) s1
+    forall f sr0 sa0 st sr1 sa1 c,
+    stmnt_runp f sr0 sa0 st sr1 sa0 ->
+    mi_stepp f sr0 sa0 (Valways c st) sr1 sa1
 | mi_stepp_Valways_ff :
-    forall f s0 st s1 c,
-    stmnt_runp f s0 st s1 ->
-    mi_stepp f s0 (Valways_ff c st) s1
+    forall f sr0 sa0 st sr1 sa1 c,
+    stmnt_runp f sr0 sa0 st sr1 sa1 ->
+    mi_stepp f sr0 sa0 (Valways_ff c st) sr1 sa1
 | mi_stepp_Valways_comb :
-    forall f s0 st s1 c,
-    stmnt_runp f s0 st s1 ->
-    mi_stepp f s0 (Valways_comb c st) s1
+    forall f sr0 sa0 st sr1 sa1 c,
+    stmnt_runp f sr0 sa0 st sr1 sa1 ->
+    mi_stepp f sr0 sa0 (Valways_comb c st) sr1 sa1
 | mi_stepp_Vdecl :
-    forall f s lhs rhs,
-    mi_stepp f s (Vdecl lhs rhs) s.
+    forall f sr sa lhs rhs,
+    mi_stepp f sr sa (Vdecl lhs rhs) sr sa.
 Hint Constructors mi_stepp : verilog.
 
-Inductive mis_stepp : fext -> associations -> list module_item -> associations -> Prop :=
+Inductive mis_stepp : fext -> reg_associations -> arr_associations ->
+                      list module_item -> reg_associations -> arr_associations -> Prop :=
 | mis_stepp_Cons :
-    forall f mi mis s0 s1 s2,
-    mi_stepp f s0 mi s1 ->
-    mis_stepp f s1 mis s2 ->
-    mis_stepp f s0 (mi :: mis) s2
+    forall f mi mis sr0 sa0 sr1 sa1 sr2 sa2,
+    mi_stepp f sr0 sa0 mi sr1 sa1 ->
+    mis_stepp f sr1 sa1 mis sr2 sa2 ->
+    mis_stepp f sr0 sa0 (mi :: mis) sr2 sa2
 | mis_stepp_Nil :
-    forall f s,
-    mis_stepp f s nil s.
+    forall f sr sa,
+    mis_stepp f sr sa nil sr sa.
 Hint Constructors mis_stepp : verilog.
 
 (*Definition mi_step_commit (s : state) (m : list module_item) : res state :=
@@ -583,19 +659,21 @@ Definition genv := Genv.t unit unit.
 
 Inductive step : state -> state -> Prop :=
 | step_module :
-    forall m stvar stvar' cycle f assoc0 assoc1 assoc2 nbassoc,
-    mis_stepp (f cycle) (mkassociations assoc0 empty_assocmap)
-              m.(mod_body)
-              (mkassociations assoc1 nbassoc) ->
-    assoc2 = merge_assocmap nbassoc assoc1 ->
-    Some stvar' = assoc2!(fst m.(mod_state)) ->
-    step (State m assoc0 empty_assocmap f cycle stvar)
-         (State m assoc2 empty_assocmap f (S cycle) stvar')
+    forall m stvar stvar' cycle f
+      asr0 asa0 asr1 asa1
+      asr' asa',
+    mis_stepp (f cycle) asr0 asa0
+              m.(mod_body) asr1 asa1 ->
+    asr' = merge_associations asr1 ->
+    asa' = merge_associations asa1 ->
+    Some stvar' = asr'.(assoc_blocking)!(fst m.(mod_state)) ->
+    step (State m asr0 asa0 f cycle stvar)
+         (State m asr' asa' f (S cycle) stvar')
 | step_finish :
-    forall m assoc f cycle stvar result,
-    assoc!(fst m.(mod_finish)) = Some (1'h"1") ->
-    assoc!(fst m.(mod_return)) = Some result ->
-    step (State m assoc empty_assocmap f cycle stvar)
+    forall m asr asa f cycle stvar result,
+    asr.(assoc_blocking)!(fst m.(mod_finish)) = Some (1'h"1") ->
+    asr.(assoc_blocking)!(fst m.(mod_return)) = Some result ->
+    step (State m asr asa f cycle stvar)
          (Finishstate result).
 Hint Constructors step : verilog.