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

4 files changed, 337 insertions, 40 deletions

diff --git a/src/verilog/Array.v b/src/verilog/Array.v
new file mode 100644
index 0000000..fc52f04
--- /dev/null
+++ b/src/verilog/Array.v
@@ -0,0 +1,271 @@
+Set Implicit Arguments.
+
+Require Import Lia.
+Require Import Coquplib.
+From Coq Require Import Lists.List Datatypes.
+
+Import ListNotations.
+
+Local Open Scope nat_scope.
+
+Record Array (A : Type) : Type :=
+  mk_array
+    { arr_contents : list A
+    ; arr_length : nat
+    ; arr_wf : length arr_contents = arr_length
+    }.
+
+Definition make_array {A : Type} (l : list A) : Array A :=
+  @mk_array A l (length l) eq_refl.
+
+Fixpoint list_set {A : Type} (i : nat) (x : A) (l : list A) {struct l} : list A :=
+  match i, l with
+  | _, nil => nil
+  | S n, h :: t => h :: list_set n x t
+  | O, h :: t => x :: t
+  end.
+
+Lemma list_set_spec1 {A : Type} :
+  forall l i (x : A),
+    i < length l -> nth_error (list_set i x l) i = Some x.
+Proof.
+  induction l; intros; destruct i; simplify; try lia; try reflexivity; firstorder.
+Qed.
+Hint Resolve list_set_spec1 : array.
+
+Lemma list_set_spec2 {A : Type} :
+  forall l i (x : A) d,
+    i < length l -> nth i (list_set i x l) d = x.
+Proof.
+  induction l; intros; destruct i; simplify; try lia; try reflexivity; firstorder.
+Qed.
+Hint Resolve list_set_spec2 : array.
+
+Lemma array_set_wf {A : Type} :
+  forall l ln i (x : A),
+    length l = ln -> length (list_set i x l) = ln.
+Proof.
+  induction l; intros; destruct i; auto.
+
+  invert H; simplify; auto.
+Qed.
+
+Definition array_set {A : Type} (i : nat) (x : A) (a : Array A) :=
+  let l := a.(arr_contents) in
+  let ln := a.(arr_length) in
+  let WF := a.(arr_wf) in
+  @mk_array A (list_set i x l) ln (@array_set_wf A l ln i x WF).
+
+Lemma array_set_spec1 {A : Type} :
+  forall a i (x : A),
+    i < a.(arr_length) -> nth_error ((array_set i x a).(arr_contents)) i = Some x.
+Proof.
+  intros.
+
+  rewrite <- a.(arr_wf) in H.
+  unfold array_set. simplify.
+  eauto with array.
+Qed.
+Hint Resolve array_set_spec1 : array.
+
+Lemma array_set_spec2 {A : Type} :
+  forall a i (x : A) d,
+    i < a.(arr_length) -> nth i ((array_set i x a).(arr_contents)) d = x.
+Proof.
+  intros.
+
+  rewrite <- a.(arr_wf) in H.
+  unfold array_set. simplify.
+  eauto with array.
+Qed.
+Hint Resolve array_set_spec2 : array.
+
+Definition array_get_error {A : Type} (i : nat) (a : Array A) : option A :=
+  nth_error a.(arr_contents) i.
+
+Lemma array_get_error_equal {A : Type} :
+  forall (a b : Array A) i,
+    a.(arr_contents) = b.(arr_contents) ->
+    array_get_error i a = array_get_error i b.
+Proof.
+  unfold array_get_error. congruence.
+Qed.
+
+Lemma array_get_error_bound {A : Type} :
+  forall (a : Array A) i,
+    i < a.(arr_length) -> exists x, array_get_error i a = Some x.
+Proof.
+  intros.
+
+  rewrite <- a.(arr_wf) in H.
+  assert (~ length (arr_contents a) <= i) by lia.
+
+  pose proof (nth_error_None a.(arr_contents) i).
+  apply not_iff_compat in H1.
+  apply <- H1 in H0.
+
+  destruct (nth_error (arr_contents a) i) eqn:EQ; try contradiction; eauto.
+Qed.
+
+Lemma array_get_error_set_bound {A : Type} :
+  forall (a : Array A) i x,
+    i < a.(arr_length) -> array_get_error i (array_set i x a) = Some x.
+Proof.
+  intros.
+
+  unfold array_get_error.
+  eauto with array.
+Qed.
+
+Definition array_get {A : Type} (i : nat) (x : A) (a : Array A) : A :=
+  nth i a.(arr_contents) x.
+
+Lemma array_get_set_bound {A : Type} :
+  forall (a : Array A) i x d,
+    i < a.(arr_length) -> array_get i d (array_set i x a) = x.
+Proof.
+  intros.
+
+  unfold array_get.
+  info_eauto with array.
+Qed.
+
+(** Tail recursive version of standard library function. *)
+Fixpoint list_repeat' {A : Type} (acc : list A) (a : A) (n : nat) : list A :=
+  match n with
+  | O => acc
+  | S n => list_repeat' (a::acc) a n
+  end.
+
+Lemma list_repeat'_len {A : Type} : forall (a : A) n l,
+    length (list_repeat' l a n) = (n + Datatypes.length l)%nat.
+Proof.
+  induction n; intros; simplify; try reflexivity.
+
+  specialize (IHn (a :: l)).
+  rewrite IHn.
+  simplify.
+  lia.
+Qed.
+
+Lemma list_repeat'_app {A : Type} : forall (a : A) n l,
+    list_repeat' l a n = list_repeat' [] a n ++ l.
+Proof.
+  induction n; intros; simplify; try reflexivity.
+
+  pose proof IHn.
+  specialize (H (a :: l)).
+  rewrite H. clear H.
+  specialize (IHn (a :: nil)).
+  rewrite IHn. clear IHn.
+  remember (list_repeat' [] a n) as l0.
+
+  rewrite <- app_assoc.
+  f_equal.
+Qed.
+
+Lemma list_repeat'_head_tail {A : Type} : forall n (a : A),
+  a :: list_repeat' [] a n = list_repeat' [] a n ++ [a].
+Proof.
+  induction n; intros; simplify; try reflexivity.
+  rewrite list_repeat'_app.
+
+  replace (a :: list_repeat' [] a n ++ [a]) with (list_repeat' [] a n ++ [a] ++ [a]).
+  2: { rewrite app_comm_cons. rewrite IHn; auto.
+       rewrite app_assoc. reflexivity. }
+  rewrite app_assoc. reflexivity.
+Qed.
+
+Lemma list_repeat'_cons {A : Type} : forall (a : A) n,
+    list_repeat' [a] a n = a :: list_repeat' [] a n.
+Proof.
+  intros.
+
+  rewrite list_repeat'_head_tail; auto.
+  apply list_repeat'_app.
+Qed.
+
+Definition list_repeat {A : Type} : A -> nat -> list A := list_repeat' nil.
+
+Lemma list_repeat_len {A : Type} : forall n (a : A), length (list_repeat a n) = n.
+Proof.
+  intros.
+  unfold list_repeat.
+  rewrite list_repeat'_len.
+  simplify. lia.
+Qed.
+
+Lemma dec_list_repeat_spec {A : Type} : forall n (a : A) a',
+    (forall x x' : A, {x' = x} + {~ x' = x}) ->
+    In a' (list_repeat a n) -> a' = a.
+Proof.
+  induction n; intros; simplify; try contradiction.
+
+  unfold list_repeat in *.
+  simplify.
+
+  rewrite list_repeat'_app in H.
+  pose proof (X a a').
+  destruct H0; auto.
+
+  (* This is actually a degenerate case, not an unprovable goal. *)
+  pose proof (in_app_or (list_repeat' [] a n) ([a])).
+  apply H0 in H. invert H.
+
+  - eapply IHn in X; eassumption.
+  - invert H1; contradiction.
+Qed.
+
+Lemma list_repeat_head_tail {A : Type} : forall n (a : A),
+    a :: list_repeat a n = list_repeat a n ++ [a].
+Proof.
+  unfold list_repeat. apply list_repeat'_head_tail.
+Qed.
+
+Lemma list_repeat_cons {A : Type} : forall n (a : A),
+    list_repeat a (S n) = a :: list_repeat a n.
+Proof.
+  intros.
+
+  unfold list_repeat.
+  apply list_repeat'_cons.
+Qed.
+
+Definition arr_repeat {A : Type} (a : A) (n : nat) : Array A := make_array (list_repeat a n).
+
+Fixpoint list_combine {A B C : Type} (f : A -> B -> C) (x : list A) (y : list B) : list C :=
+  match x, y with
+  | a :: t, b :: t' => f a b :: list_combine f t t'
+  | _, _ => nil
+  end.
+
+Lemma list_combine_length {A B C : Type} (f : A -> B -> C) : forall (x : list A) (y : list B),
+    length (list_combine f x y) = min (length x) (length y).
+Proof.
+  induction x; intros; simplify; try reflexivity.
+
+  destruct y; simplify; auto.
+Qed.
+
+Definition combine {A B C : Type} (f : A -> B -> C) (x : Array A) (y : Array B) : Array C :=
+  make_array (list_combine f x.(arr_contents) y.(arr_contents)).
+
+Lemma combine_length {A B C: Type} : forall x y (f : A -> B -> C),
+    x.(arr_length) = y.(arr_length) -> arr_length (combine f x y) = x.(arr_length).
+Proof.
+  intros.
+
+  unfold combine.
+  unfold make_array.
+  simplify.
+
+  rewrite <- (arr_wf x) in *.
+  rewrite <- (arr_wf y) in *.
+
+  destruct (arr_contents x); simplify.
+  - reflexivity.
+  - destruct (arr_contents y); simplify.
+    f_equal.
+    rewrite list_combine_length.
+    destruct (Min.min_dec (length l) (length l0)); congruence.
+Qed.
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
index c07d672..0bf5072 100644
--- a/src/verilog/HTL.v
+++ b/src/verilog/HTL.v
@@ -17,7 +17,7 @@
  *)
 
 From Coq Require Import FSets.FMapPositive.
-From coqup Require Import Coquplib Value AssocMap.
+From coqup Require Import Coquplib Value AssocMap Array.
 From coqup Require Verilog.
 From compcert Require Events Globalenvs Smallstep Integers Values.
 From compcert Require Import Maps.
@@ -46,6 +46,7 @@ Record module: Type :=
     mod_entrypoint : node;
     mod_st : reg;
     mod_stk : reg;
+    mod_stk_len : nat;
     mod_finish : reg;
     mod_return : reg;
     mod_start : reg;
@@ -65,6 +66,9 @@ Fixpoint init_regs (vl : list value) (rl : list reg) {struct rl} :=
   | _, _ => empty_assocmap
   end.
 
+Definition empty_stack (m : module) : Verilog.assocmap_arr :=
+  (AssocMap.set m.(mod_stk) (Array.arr_repeat None m.(mod_stk_len)) (AssocMap.empty Verilog.arr)).
+
 (** * Operational Semantics *)
 
 Definition genv := Globalenvs.Genv.t fundef unit.
@@ -74,7 +78,8 @@ Inductive stackframe : Type :=
     forall  (res : reg)
             (m : module)
             (pc : node)
-            (assoc : assocmap),
+            (reg_assoc : Verilog.assocmap_reg)
+            (arr_assoc : Verilog.assocmap_arr),
       stackframe.
 
 Inductive state : Type :=
@@ -82,8 +87,8 @@ Inductive state : Type :=
     forall (stack : list stackframe)
            (m : module)
            (st : node)
-           (reg_assoc : assocmap)
-           (arr_assoc : AssocMap.t (list value)), state
+           (reg_assoc : Verilog.assocmap_reg)
+           (arr_assoc : Verilog.assocmap_arr), state
 | Returnstate :
     forall (res : list stackframe)
            (v : value), state
@@ -104,7 +109,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
       m.(mod_datapath)!st = Some data ->
       Verilog.stmnt_runp f
         (Verilog.mkassociations asr empty_assocmap)
-        (Verilog.mkassociations asa (AssocMap.empty (list value)))
+        (Verilog.mkassociations asa (empty_stack m))
         ctrl
         (Verilog.mkassociations basr1 nasr1)
         (Verilog.mkassociations basa1 nasa1) ->
@@ -114,8 +119,8 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
         data
         (Verilog.mkassociations basr2 nasr2)
         (Verilog.mkassociations basa2 nasa2) ->
-      asr' = merge_assocmap nasr2 basr2 ->
-      asa' = AssocMapExt.merge (list value) nasa2 basa2 ->
+      asr' = Verilog.merge_regs nasr2 basr2 ->
+      asa' = Verilog.merge_arrs nasa2 basa2 ->
       asr'!(m.(mod_st)) = Some stval ->
       valueToPos stval = pstval ->
       step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa')
@@ -130,13 +135,12 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
            (State res m m.(mod_entrypoint)
              (AssocMap.set (mod_st m) (posToValue 32 m.(mod_entrypoint))
                            (init_regs args m.(mod_params)))
-              (AssocMap.empty (list value)))
+             (empty_stack m))
 | step_return :
-    forall g m asr i r sf pc mst,
+    forall g m asr asa i r sf pc mst,
       mst = mod_st m ->
-      step g (Returnstate (Stackframe r m pc asr :: sf) i) Events.E0
-           (State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i)
-                  (AssocMap.empty (list value))).
+      step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0
+           (State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i) asa).
 Hint Constructors step : htl.
 
 Inductive initial_state (p: program): state -> Prop :=
diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index d527b15..b1ee353 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -296,6 +296,11 @@ Inductive val_value_lessdef: val -> value -> Prop :=
     val_value_lessdef (Vint i) v'
 | lessdef_undef: forall v, val_value_lessdef Vundef v.
 
+Inductive opt_val_value_lessdef: option val -> value -> Prop :=
+| opt_lessdef_some:
+    forall v v', val_value_lessdef v v' -> opt_val_value_lessdef (Some v) v'
+| opt_lessdef_none: forall v, opt_val_value_lessdef None v.
+
 Lemma valueToZ_ZToValue :
   forall n z,
   (- Z.of_nat (2 ^ n) <= z < Z.of_nat (2 ^ n))%Z ->
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index b80678e..7d5e3c0 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -25,9 +25,11 @@ From Coq Require Import
   Lists.List
   Program.
 
+Require Import Lia.
+
 Import ListNotations.
 
-From coqup Require Import common.Coquplib common.Show verilog.Value AssocMap.
+From coqup Require Import common.Coquplib common.Show verilog.Value AssocMap Array.
 From compcert Require Integers Events.
 From compcert Require Import Errors Smallstep Globalenvs.
 
@@ -47,39 +49,51 @@ Record associations (A : Type) : Type :=
     assoc_nonblocking : AssocMap.t A
   }.
 
+Definition arr := (Array (option value)).
+
 Definition reg_associations := associations value.
-Definition arr_associations := associations (list value).
+Definition arr_associations := associations arr.
 
-Definition assocmap_arr := AssocMap.t (list value).
+Definition assocmap_reg := AssocMap.t value.
+Definition assocmap_arr := AssocMap.t arr.
 
-Definition merge_associations {A : Type} (assoc : associations A) :=
-  mkassociations (AssocMapExt.merge A assoc.(assoc_nonblocking) assoc.(assoc_blocking))
-                 (AssocMap.empty A).
+Definition merge_regs (new : assocmap_reg) (old : assocmap_reg) : assocmap_reg :=
+  AssocMapExt.merge value new old.
+
+Definition merge_cell (new : option value) (old : option value) : option value :=
+  match new, old with
+  | Some _, _ => new
+  | _, _ => old
+  end.
+
+Definition merge_arr (new : option arr) (old : option arr) : option arr :=
+  match new, old with
+  | Some new', Some old' => Some (combine merge_cell new' old')
+  | Some new', None => Some new'
+  | None, Some old' => Some old'
+  | None, None => None
+  end.
+
+Definition merge_arrs (new : assocmap_arr) (old : assocmap_arr) : assocmap_arr :=
+  AssocMap.combine merge_arr new old.
 
 Definition arr_assocmap_lookup (a : assocmap_arr) (r : reg) (i : nat) : option value :=
   match a ! r with
   | None => None
-  | Some arr => nth_error arr i
-  end.
-
-Fixpoint list_set {A : Type} (i : nat) (x : A) (l : list A) : list A :=
-  match i, l with
-  | _, nil => nil
-  | S n, h :: t => h :: list_set n x t
-  | O, h :: t => x :: t
+  | Some arr => Some (Option.default (NToValue 32 0) (Option.join (array_get_error i arr)))
   end.
 
-Definition assocmap_l_set (r : reg) (i : nat) (v : value) (a : assocmap_arr) : assocmap_arr :=
+Definition arr_assocmap_set (r : reg) (i : nat) (v : value) (a : assocmap_arr) : assocmap_arr :=
   match a ! r with
   | None => a
-  | Some arr => AssocMap.set r (list_set i v arr) a
+  | Some arr => a # r <- (array_set i (Some v) arr)
   end.
 
 Definition block_arr (r : reg) (i : nat) (asa : arr_associations) (v : value) : arr_associations :=
-  mkassociations (assocmap_l_set r i v asa.(assoc_blocking)) asa.(assoc_nonblocking).
+  mkassociations (arr_assocmap_set r i v asa.(assoc_blocking)) asa.(assoc_nonblocking).
 
 Definition nonblock_arr (r : reg) (i : nat) (asa : arr_associations) (v : value) : arr_associations :=
-  mkassociations asa.(assoc_blocking) (assocmap_l_set r i v asa.(assoc_nonblocking)).
+  mkassociations asa.(assoc_blocking) (arr_assocmap_set r i v asa.(assoc_nonblocking)).
 
 Definition block_reg (r : reg) (asr : reg_associations) (v : value) :=
   mkassociations (AssocMap.set r v asr.(assoc_blocking)) asr.(assoc_nonblocking).
@@ -87,8 +101,8 @@ Definition block_reg (r : reg) (asr : reg_associations) (v : value) :=
 Definition nonblock_reg (r : reg) (asr : reg_associations) (v : value) :=
   mkassociations asr.(assoc_blocking) (AssocMap.set r v asr.(assoc_nonblocking)).
 
-Inductive scl_decl : Type := Scalar (sz : nat).
-Inductive arr_decl : Type := Array (sz : nat) (ln : nat).
+Inductive scl_decl : Type := VScalar (sz : nat).
+Inductive arr_decl : Type := VArray (sz : nat) (ln : nat).
 
 (** * Verilog AST
 
@@ -218,6 +232,7 @@ Record module : Type := mkmodule {
   mod_return : reg;
   mod_st : reg; (**r Variable that defines the current state, it should be internal. *)
   mod_stk : reg;
+  mod_stk_len : nat;
   mod_args : list reg;
   mod_body : list module_item;
   mod_entrypoint : node;
@@ -235,7 +250,7 @@ Definition posToLit (p : positive) : expr :=
 Coercion Vlit : value >-> expr.
 Coercion Vvar : reg >-> expr.
 
-Definition fext := AssocMap.t value.
+Definition fext := assocmap.
 Definition fextclk := nat -> fext.
 
 (** ** State
@@ -272,8 +287,8 @@ Inductive state : Type :=
     forall (stack : list stackframe)
            (m : module)
            (st : node)
-           (reg_assoc : assocmap)
-           (arr_assoc : AssocMap.t (list value)), state
+           (reg_assoc : assocmap_reg)
+           (arr_assoc : assocmap_arr), state
 | Returnstate :
     forall (res : list stackframe)
            (v : value), state
@@ -691,17 +706,19 @@ Fixpoint init_params (vl : list value) (rl : list reg) {struct rl} :=
   end.
 
 Definition genv := Globalenvs.Genv.t fundef unit.
+Definition empty_stack (m : module) : assocmap_arr :=
+  (AssocMap.set m.(mod_stk) (Array.arr_repeat None m.(mod_stk_len)) (AssocMap.empty arr)).
 
 Inductive step : genv -> state -> Events.trace -> state -> Prop :=
   | step_module :
       forall asr asa asr' asa' basr1 nasr1 basa1 nasa1 f stval pstval m sf st g,
       mis_stepp f (mkassociations asr empty_assocmap)
-                  (mkassociations asa (AssocMap.empty (list value)))
+                  (mkassociations asa (empty_stack m))
                   m.(mod_body)
                   (mkassociations basr1 nasr1)
                   (mkassociations basa1 nasa1)->
-      asr' = merge_assocmap nasr1 basr1 ->
-      asa' = AssocMapExt.merge (list value) nasa1 basa1 ->
+      asr' = merge_regs nasr1 basr1 ->
+      asa' = merge_arrs nasa1 basa1 ->
       asr'!(m.(mod_st)) = Some stval ->
       valueToPos stval = pstval ->
       step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa')
@@ -716,13 +733,13 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
          (State res m m.(mod_entrypoint)
           (AssocMap.set m.(mod_st) (posToValue 32 m.(mod_entrypoint))
            (init_params args m.(mod_args)))
-          (AssocMap.empty (list value)))
+          (empty_stack m))
 | step_return :
     forall g m asr i r sf pc mst,
     mst = mod_st m ->
     step g (Returnstate (Stackframe r m pc asr :: sf) i) Events.E0
          (State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i)
-                (AssocMap.empty (list value))).
+                (empty_stack m)).
 Hint Constructors step : verilog.
 
 Inductive initial_state (p: program): state -> Prop :=