From d0257b0a47ad998e01715e9bc6ba612b834765f1 Mon Sep 17 00:00:00 2001
From: James Pollard <james@pollard.dev>
Date: Thu, 11 Jun 2020 14:47:52 +0100
Subject: Working on proof.

---
 src/verilog/HTL.v   | 21 +++++++++++++++------
 src/verilog/Value.v |  5 +++++
 2 files changed, 20 insertions(+), 6 deletions(-)

(limited to 'src/verilog')

diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
index 2e4ef1a..82aac41 100644
--- a/src/verilog/HTL.v
+++ b/src/verilog/HTL.v
@@ -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
   }.
@@ -60,6 +61,14 @@ Fixpoint init_regs (vl : list value) (rl : list reg) {struct rl} :=
   | _, _ => empty_assocmap
   end.
 
+Fixpoint zeroes' (acc : list value) (n : nat) : list value :=
+  match n with
+  | O => acc
+  | S n => zeroes' ((NToValue 32 0)::acc) n
+  end.
+
+Definition zeroes : nat -> list value := zeroes' nil.
+
 (** * Operational Semantics *)
 
 Definition genv := Globalenvs.Genv.t fundef unit.
@@ -69,7 +78,8 @@ Inductive stackframe : Type :=
     forall  (res : reg)
             (m : module)
             (pc : node)
-            (assoc : assocmap),
+            (reg_assoc : assocmap)
+            (arr_assoc : AssocMap.t (list value)),
       stackframe.
 
 Inductive state : Type :=
@@ -125,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)))
+              (AssocMap.set m.(mod_stk) (zeroes m.(mod_stk_len)) (AssocMap.empty (list value))))
 | 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 ->
-- 
cgit 


From 088a554043e3d4b8b8b424dbda9a136e3f4571e5 Mon Sep 17 00:00:00 2001
From: James Pollard <james@pollard.dev>
Date: Thu, 11 Jun 2020 22:50:01 +0100
Subject: Rough outline of stack address proof

---
 src/verilog/Verilog.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'src/verilog')

diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 845d706..0e999de 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -56,10 +56,10 @@ 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 :=
+Definition arr_assocmap_lookup (a : assocmap_arr) (r : reg) (i : nat) : value :=
   match a ! r with
-  | None => None
-  | Some arr => nth_error arr i
+  | None => natToValue 32 0
+  | Some arr => nth i arr (natToValue 32 0)
   end.
 
 Fixpoint list_set {A : Type} (i : nat) (x : A) (l : list A) : list A :=
@@ -297,7 +297,7 @@ Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop
   | 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 ->
+      arr_assocmap_lookup stack r (valueToNat i) = v ->
       expr_runp fext reg stack (Vvari r iexp) v
   | erun_Vinputvar :
       forall fext reg stack r v,
-- 
cgit 


From 21ae45cd03f7d38b1ef12270307274a9ee370e17 Mon Sep 17 00:00:00 2001
From: James Pollard <james@pollard.dev>
Date: Sat, 13 Jun 2020 21:36:32 +0100
Subject: Add a basic length-indexed list type.

---
 src/verilog/Array.v | 123 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 123 insertions(+)
 create mode 100644 src/verilog/Array.v

(limited to 'src/verilog')

diff --git a/src/verilog/Array.v b/src/verilog/Array.v
new file mode 100644
index 0000000..8673f0c
--- /dev/null
+++ b/src/verilog/Array.v
@@ -0,0 +1,123 @@
+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_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.
-- 
cgit 


From 044a68b1b215125e2651c637f28c794536d27ba5 Mon Sep 17 00:00:00 2001
From: James Pollard <james@pollard.dev>
Date: Sun, 14 Jun 2020 16:41:27 +0100
Subject: Array semantics now uses dependent Array type.

---
 src/verilog/HTL.v     | 21 ++++++++-----------
 src/verilog/Verilog.v | 57 ++++++++++++++++++++++++++++-----------------------
 2 files changed, 39 insertions(+), 39 deletions(-)

(limited to 'src/verilog')

diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
index c509248..8149ddf 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.
@@ -66,13 +66,8 @@ Fixpoint init_regs (vl : list value) (rl : list reg) {struct rl} :=
   | _, _ => empty_assocmap
   end.
 
-Fixpoint zeroes' (acc : list value) (n : nat) : list value :=
-  match n with
-  | O => acc
-  | S n => zeroes' ((NToValue 32 0)::acc) n
-  end.
-
-Definition zeroes : nat -> list value := zeroes' nil.
+Definition empty_stack (m : module) : AssocMap.t (Array value) :=
+  (AssocMap.set m.(mod_stk) (Verilog.zeroes m.(mod_stk_len)) (AssocMap.empty (Array value))).
 
 (** * Operational Semantics *)
 
@@ -84,7 +79,7 @@ Inductive stackframe : Type :=
             (m : module)
             (pc : node)
             (reg_assoc : assocmap)
-            (arr_assoc : AssocMap.t (list value)),
+            (arr_assoc : AssocMap.t (Array value)),
       stackframe.
 
 Inductive state : Type :=
@@ -93,7 +88,7 @@ Inductive state : Type :=
            (m : module)
            (st : node)
            (reg_assoc : assocmap)
-           (arr_assoc : AssocMap.t (list value)), state
+           (arr_assoc : AssocMap.t (Array value)), state
 | Returnstate :
     forall (res : list stackframe)
            (v : value), state
@@ -114,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) ->
@@ -125,7 +120,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
         (Verilog.mkassociations basr2 nasr2)
         (Verilog.mkassociations basa2 nasa2) ->
       asr' = merge_assocmap nasr2 basr2 ->
-      asa' = AssocMapExt.merge (list value) nasa2 basa2 ->
+      asa' = AssocMapExt.merge (Array value) 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')
@@ -140,7 +135,7 @@ 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.set m.(mod_stk) (zeroes m.(mod_stk_len)) (AssocMap.empty (list value))))
+             (empty_stack m))
 | step_return :
     forall g m asr asa i r sf pc mst,
       mst = mod_st m ->
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 8b83d49..3ab3f10 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -27,7 +27,7 @@ From Coq Require Import
 
 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.
 
@@ -48,38 +48,31 @@ Record associations (A : Type) : Type :=
   }.
 
 Definition reg_associations := associations value.
-Definition arr_associations := associations (list value).
+Definition arr_associations := associations (Array value).
 
-Definition assocmap_arr := AssocMap.t (list value).
+Definition assocmap_arr := AssocMap.t (Array 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) : value :=
+Definition arr_assocmap_lookup (a : assocmap_arr) (r : reg) (i : nat) : option value :=
   match a ! r with
-  | None => natToValue 32 0
-  | Some arr => nth i arr (natToValue 32 0)
+  | None => None
+  | Some arr => array_get_error i arr
   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 :=
+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 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 +80,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
 
@@ -217,6 +210,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;
@@ -234,7 +228,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,7 +266,7 @@ Inductive state : Type :=
            (m : module)
            (st : node)
            (reg_assoc : assocmap)
-           (arr_assoc : AssocMap.t (list value)), state
+           (arr_assoc : AssocMap.t (Array value)), state
 | Returnstate :
     forall (res : list stackframe)
            (v : value), state
@@ -324,7 +318,7 @@ Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop
   | erun_Vvari :
       forall fext reg stack v iexp i r,
       expr_runp fext reg stack iexp i ->
-      arr_assocmap_lookup stack r (valueToNat i) = v ->
+      arr_assocmap_lookup stack r (valueToNat i) = Some v ->
       expr_runp fext reg stack (Vvari r iexp) v
   | erun_Vinputvar :
       forall fext reg stack r v,
@@ -690,16 +684,27 @@ Fixpoint init_params (vl : list value) (rl : list reg) {struct rl} :=
 
 Definition genv := Globalenvs.Genv.t fundef unit.
 
+Fixpoint list_zeroes' (acc : list value) (n : nat) : list value :=
+  match n with
+  | O => acc
+  | S n => list_zeroes' ((NToValue 32 0)::acc) n
+  end.
+
+Definition list_zeroes : nat -> list value := list_zeroes' nil.
+Definition zeroes (n : nat) : Array value := make_array (list_zeroes n).
+Definition empty_stack (m : module) : AssocMap.t (Array value) :=
+  (AssocMap.set m.(mod_stk) (zeroes m.(mod_stk_len)) (AssocMap.empty (Array value))).
+
 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 ->
+      asa' = AssocMapExt.merge (Array value) 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')
@@ -714,13 +719,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 :=
-- 
cgit 


From dfea5f0f6307177a9127ce29db496a819dcdb232 Mon Sep 17 00:00:00 2001
From: James Pollard <james@pollard.dev>
Date: Wed, 17 Jun 2020 19:53:43 +0100
Subject: Fix array semantics merge granularity.

---
 src/verilog/Array.v   | 38 ++++++++++++++++++++++++++++++++++
 src/verilog/HTL.v     | 16 +++++++--------
 src/verilog/Verilog.v | 56 +++++++++++++++++++++++++++++++--------------------
 3 files changed, 80 insertions(+), 30 deletions(-)

(limited to 'src/verilog')

diff --git a/src/verilog/Array.v b/src/verilog/Array.v
index 8673f0c..16f5406 100644
--- a/src/verilog/Array.v
+++ b/src/verilog/Array.v
@@ -121,3 +121,41 @@ Proof.
   unfold array_get.
   info_eauto with array.
 Qed.
+
+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 : forall {A : Type} (a : A) n l,
+    Datatypes.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.
+
+Definition list_repeat {A : Type} : A -> nat -> list A := list_repeat' nil.
+
+Lemma list_repeat_len {A : Type} : forall n (a : A), Datatypes.length (list_repeat a n) = n.
+Proof.
+  intros.
+  unfold list_repeat.
+  rewrite list_repeat'_len.
+  simplify. lia.
+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.
+
+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)).
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
index 8149ddf..0bf5072 100644
--- a/src/verilog/HTL.v
+++ b/src/verilog/HTL.v
@@ -66,8 +66,8 @@ Fixpoint init_regs (vl : list value) (rl : list reg) {struct rl} :=
   | _, _ => empty_assocmap
   end.
 
-Definition empty_stack (m : module) : AssocMap.t (Array value) :=
-  (AssocMap.set m.(mod_stk) (Verilog.zeroes m.(mod_stk_len)) (AssocMap.empty (Array value))).
+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 *)
 
@@ -78,8 +78,8 @@ Inductive stackframe : Type :=
     forall  (res : reg)
             (m : module)
             (pc : node)
-            (reg_assoc : assocmap)
-            (arr_assoc : AssocMap.t (Array value)),
+            (reg_assoc : Verilog.assocmap_reg)
+            (arr_assoc : Verilog.assocmap_arr),
       stackframe.
 
 Inductive state : Type :=
@@ -87,8 +87,8 @@ Inductive state : Type :=
     forall (stack : list stackframe)
            (m : module)
            (st : node)
-           (reg_assoc : assocmap)
-           (arr_assoc : AssocMap.t (Array value)), state
+           (reg_assoc : Verilog.assocmap_reg)
+           (arr_assoc : Verilog.assocmap_arr), state
 | Returnstate :
     forall (res : list stackframe)
            (v : value), state
@@ -119,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 (Array 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')
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 3ab3f10..d20ffcd 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -25,6 +25,8 @@ From Coq Require Import
   Lists.List
   Program.
 
+Require Import Lia.
+
 Import ListNotations.
 
 From coqup Require Import common.Coquplib common.Show verilog.Value AssocMap Array.
@@ -47,25 +49,44 @@ Record associations (A : Type) : Type :=
     assoc_nonblocking : AssocMap.t A
   }.
 
+Definition arr := (Array (option value)).
+
 Definition reg_associations := associations value.
-Definition arr_associations := associations (Array value).
+Definition arr_associations := associations arr.
+
+Definition assocmap_reg := AssocMap.t value.
+Definition assocmap_arr := AssocMap.t arr.
 
-Definition assocmap_arr := AssocMap.t (Array value).
+Definition merge_regs (new : assocmap_reg) (old : assocmap_reg) : assocmap_reg :=
+  AssocMapExt.merge value new old.
 
-Definition merge_associations {A : Type} (assoc : associations A) :=
-  mkassociations (AssocMapExt.merge A assoc.(assoc_nonblocking) assoc.(assoc_blocking))
-                 (AssocMap.empty A).
+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 => array_get_error i arr
+  | Some arr => Option.join (array_get_error i arr)
   end.
 
 Definition arr_assocmap_set (r : reg) (i : nat) (v : value) (a : assocmap_arr) : assocmap_arr :=
   match a ! r with
   | None => a
-  | Some arr => a # r <- (array_set i v arr)
+  | 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 :=
@@ -265,8 +286,8 @@ Inductive state : Type :=
     forall (stack : list stackframe)
            (m : module)
            (st : node)
-           (reg_assoc : assocmap)
-           (arr_assoc : AssocMap.t (Array value)), state
+           (reg_assoc : assocmap_reg)
+           (arr_assoc : assocmap_arr), state
 | Returnstate :
     forall (res : list stackframe)
            (v : value), state
@@ -683,17 +704,8 @@ Fixpoint init_params (vl : list value) (rl : list reg) {struct rl} :=
   end.
 
 Definition genv := Globalenvs.Genv.t fundef unit.
-
-Fixpoint list_zeroes' (acc : list value) (n : nat) : list value :=
-  match n with
-  | O => acc
-  | S n => list_zeroes' ((NToValue 32 0)::acc) n
-  end.
-
-Definition list_zeroes : nat -> list value := list_zeroes' nil.
-Definition zeroes (n : nat) : Array value := make_array (list_zeroes n).
-Definition empty_stack (m : module) : AssocMap.t (Array value) :=
-  (AssocMap.set m.(mod_stk) (zeroes m.(mod_stk_len)) (AssocMap.empty (Array value))).
+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 :
@@ -703,8 +715,8 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
                   m.(mod_body)
                   (mkassociations basr1 nasr1)
                   (mkassociations basa1 nasa1)->
-      asr' = merge_assocmap nasr1 basr1 ->
-      asa' = AssocMapExt.merge (Array 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')
-- 
cgit 


From 00c579e603478d452959dde0ec61672d7b5d27a4 Mon Sep 17 00:00:00 2001
From: James Pollard <james@pollard.dev>
Date: Wed, 17 Jun 2020 23:08:32 +0100
Subject: Some (very) useful lemmas about arrays.

---
 src/verilog/Array.v | 108 ++++++++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 105 insertions(+), 3 deletions(-)

(limited to 'src/verilog')

diff --git a/src/verilog/Array.v b/src/verilog/Array.v
index 16f5406..0b6e2a9 100644
--- a/src/verilog/Array.v
+++ b/src/verilog/Array.v
@@ -122,14 +122,15 @@ Proof.
   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 : forall {A : Type} (a : A) n l,
-    Datatypes.length (list_repeat' l a n) = (n + Datatypes.length l)%nat.
+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.
 
@@ -139,9 +140,46 @@ Proof.
   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), Datatypes.length (list_repeat a n) = n.
+Lemma list_repeat_len {A : Type} : forall n (a : A), length (list_repeat a n) = n.
 Proof.
   intros.
   unfold list_repeat.
@@ -149,6 +187,42 @@ Proof.
   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 :=
@@ -157,5 +231,33 @@ Fixpoint list_combine {A B C : Type} (f : A -> B -> C) (x : list A) (y : list B)
   | _, _ => 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.
-- 
cgit 


From 9a65ca2731adf234f5ce946503314267ced62a44 Mon Sep 17 00:00:00 2001
From: James Pollard <james@pollard.dev>
Date: Wed, 17 Jun 2020 23:19:48 +0100
Subject: Fix Inop proof to work with new array semantics.

---
 src/verilog/Array.v | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'src/verilog')

diff --git a/src/verilog/Array.v b/src/verilog/Array.v
index 0b6e2a9..705dea7 100644
--- a/src/verilog/Array.v
+++ b/src/verilog/Array.v
@@ -83,6 +83,14 @@ 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.
-- 
cgit 


From 9e49a65aa01e79b85a35d1dd15f45ee89e3e9906 Mon Sep 17 00:00:00 2001
From: James Pollard <james@pollard.dev>
Date: Thu, 18 Jun 2020 00:01:11 +0100
Subject: Fix array semantics behaviour for undefined values.

---
 src/verilog/Verilog.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/verilog')

diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index d20ffcd..4144632 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -80,7 +80,7 @@ Definition merge_arrs (new : assocmap_arr) (old : assocmap_arr) : assocmap_arr :
 Definition arr_assocmap_lookup (a : assocmap_arr) (r : reg) (i : nat) : option value :=
   match a ! r with
   | None => None
-  | Some arr => Option.join (array_get_error i arr)
+  | Some arr => Some (Option.default (NToValue 32 0) (Option.join (array_get_error i arr)))
   end.
 
 Definition arr_assocmap_set (r : reg) (i : nat) (v : value) (a : assocmap_arr) : assocmap_arr :=
-- 
cgit 


From 6b20fbbeaad23724ca7fbcc10c9445f5cb94b699 Mon Sep 17 00:00:00 2001
From: James Pollard <james@pollard.dev>
Date: Thu, 18 Jun 2020 17:12:20 +0100
Subject: Tidy up proof.

---
 src/verilog/Array.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/verilog')

diff --git a/src/verilog/Array.v b/src/verilog/Array.v
index 705dea7..fc52f04 100644
--- a/src/verilog/Array.v
+++ b/src/verilog/Array.v
@@ -104,7 +104,7 @@ Proof.
   apply not_iff_compat in H1.
   apply <- H1 in H0.
 
-  destruct (nth_error (arr_contents a) i ) eqn:EQ; try contradiction; eauto.
+  destruct (nth_error (arr_contents a) i) eqn:EQ; try contradiction; eauto.
 Qed.
 
 Lemma array_get_error_set_bound {A : Type} :
-- 
cgit